Verification

• BDD-Based Verification
  • Current API
  • High-level behavior
  • Notes
• Program Verification
  • Verification pipeline
  • Main engines
  • CLI entrypoints
  • Where to look next
• PDR (Property-Directed Reachability)
  • Current engine surface
  • Idea
  • Programmatic usage
  • CLI usage
• SMT Tools
  • Directory structure
  • PySMTSolver
  • SyGuS Solver
  • Exceptions
  • Programmatic usage
• PolyHorn: Polynomial Horn Clause Solver
  • Introduction
  • Core Concepts
  • API Reference
  • Usage Examples
  • Implementation Details
  • Limitations and Considerations
  • Related Work
  • References
• Houdini
  • Current engine surface
  • How it fits in EFMC
  • Programmatic usage
  • CLI usage
• K-Induction
  • Current engine surface
  • Idea
  • Programmatic usage
  • CLI usage
• K-Safety Verification
  • Overview
  • Architecture
  • Available Provers
  • Usage
  • HyperLTL Example
  • Verification Methods
  • Properties
  • Related Work
• Ranking Functions
  • Current status
  • How to approach ranking-related workflows today
  • CLI entrypoint
  • Notes
• 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