Verification

• BDD-based Symbolic Model Checking
  • Overview
  • Algorithm
  • Usage
  • Configuration Options
  • Limitations
  • Future Improvements
  • References
• Program Verification
  • Available Verification Engines
  • Correctness
• PolyHorn: Polynomial Horn Clause Solver
  • Introduction
  • Core Concepts
  • API Reference
  • Usage Examples
  • Implementation Details
  • Limitations and Considerations
  • Related Work
  • References
• Houdini
  • References
• K-induction
  • Formal Verification Techniques
  • Components of Mathematical Induction
  • Example: Sum of the First n Natural Numbers
  • Basic Inductive Verification Approach
  • Formal Definition
  • Challenges in Inductive Verification
  • Motivation for K-Induction
  • Components of K-Induction
  • Formal Definition
  • Choosing k
• K-Safety Verification
  • Overview
  • Architecture
  • Available Provers
  • Usage
  • HyperLTL Example
  • Verification Methods
  • Properties
  • Related Work
• Ranking Function Templates for Termination Verification
  • Overview
  • Implemented Templates
  • Usage
  • Implementation Details
  • Limitations and Future Work
  • Examples
  • References
• Danger Invariants
  • Overview
  • Verification Conditions
  • Result Interpretation
  • Usage
  • API Reference
  • Bit-Vector Support
  • Example: Proving Unsafety
  • Applications
  • Related Work
• Linear Teamporal Logic
• Symbolic Finite Automata
  • Overview
  • Core Components
  • Utility Modules
  • Advanced Features
  • Implementation Backends
  • String Analysis
  • Performance Considerations
  • Common Patterns
  • Error Handling
  • Troubleshooting
  • API Reference
• LLM4Inv: LLM-Guided Invariant Synthesis
  • Overview
  • Architecture
  • Usage
  • Command-Line Options
  • How It Works
  • Supported Models
  • Limitations
  • Related Work