Invariant checking for SMT-based systems with quantifiers
From MaRDI portal
(Redirected from Publication:6636621)
Cites work
- An automatic proving approach to parameterized verification
- Backward reachability of array-based systems by SMT solving: termination and invariant synthesis
- Bounded quantifier instantiation for checking inductive invariants
- Computer Aided Verification
- Counterexample-guided abstraction refinement for symbolic model checking
- Decidability of inferring inductive invariants
- Decidability of parameterized verification
- Eager abstraction for symbolic model checking
- Efficient generation of Craig interpolants in satisfiability modulo theories
- Formal Methods in Computer-Aided Design
- Formal specification and verification of dynamic parametrized architectures
- scientific article; zbMATH DE number 1701752 (Why is no real title available?)
- Infinite-state invariant checking with IC3 and predicate abstraction
- Lazy Abstraction with Interpolants
- Predicate abstraction with indexed predicates
- Property-directed inference of universal invariants or proving their absence
- SAT-Based Model Checking without Unrolling
- Simplify: a theorem prover for program checking
- Solving quantified verification conditions using satisfiability modulo theories
- Synthesizing history and prophecy variables for symbolic model checking
- Towards SMT Model Checking of Array-Based Systems
- Universal guards, relativization of quantifiers, and failure models in model checking modulo theories
- Universal invariant checking of parametric systems with quantifier-free SMT reasoning
- Verification of SMT systems with quantifiers
This page was built for publication: Invariant checking for SMT-based systems with quantifiers
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6636621)
