Cited in
(27)- 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
- Discovering invariants via simple component analysis
- An iterative approach to precondition inference using constrained Horn clauses
- Backward symbolic execution with loop folding
- Valigator
- Dagger
- TRACER
- Lackwit
- LOOPUS
- Lingva
- Snugglebug
- DynaMate
- STeP
- c2i
- JKind
- Tip
- QuIt
- Loop Analysis by Quantification over Iterations
- Computing minimal separating DFAs and regular invariants using SAT and SMT solvers
- Infinite-state invariant checking with IC3 and predicate abstraction
- Reasoning about loops using Vampire in KeY
- 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
