Welcome to EFMC’s documentation

Contents:

• Program Verification
  • Correctness
• Abstraction Interpretation
  • Chaotic Iteration
• Widening
  • Systematic Abstraction
• Making Abstraction Interpretation Complete
  • Abstract Interpretation Tools
  • References
• Linear Teamporal Logic
• Abuduction
  • 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
• Predicate Abstraction and CEGAR
  • Predicate Abstraction
  • Abstraction Refinement
  • References
• Program Synthesis
  • Programming by Examples
  • Synthesizing Inductive Invariants
• Template-based Invariant Generation
  • Linear Arithmetic
  • Nonlinear Arithmetic
• PolyHorn Engine
  • Overview
  • Theoretical Background
  • Usage
  • Implementation Details
  • Advanced Features
  • Examples
  • Performance Considerations
  • Limitations
  • Integration with EFMC
  • References
• More Third-Party Tools
  • SyGuS
• Houdini
  • References
• Ranking Function Templates for Termination Verification
  • Overview
  • Implemented Templates
  • Usage
  • Implementation Details
  • Limitations and Future Work
  • Examples
  • References
• Playing wiht Program Verification with EFMC
  • 1. Setup and Installation
  • 2. Understanding Input Formats
  • 3. Basic Verification
  • 4. Advanced Verification Techniques
  • 5. Best Practices
  • 6. Example Workflow
  • 7. References

Indices and tables

• Index

• Module Index

• Search Page