InvGen

swMATH9780MaRDI QIDQ21759FDOQ21759

Author name not available (Why is that?)

Cited In (14)

• A learning-based approach to synthesizing invariants for incomplete verification engines
• Deriving invariants by algorithmic learning, decision procedures, and predicate abstraction
• A data driven approach for algebraic loop invariants
• An iterative approach to precondition inference using constrained Horn clauses
• Discovering invariants via simple component analysis
• Backward symbolic execution with loop folding
• Loop Analysis by Quantification over Iterations
• Computing minimal separating DFAs and regular invariants using SAT and SMT solvers
• Reasoning about loops using Vampire in KeY
• Infinite-state invariant checking with IC3 and predicate abstraction
• Aligators for Arrays (Tool Paper)
• Lingva: generating and proving program properties using symbol elimination
• Generalizing the template polyhedral domain
• Horn clause verification with convex polyhedral abstraction and tree automata-based refinement

This page was built for software: InvGen