On invariant synthesis for parametric systems
From MaRDI portal
Publication:2305429
DOI10.1007/978-3-030-29436-6_23OpenAlexW2969349375MaRDI QIDQ2305429
Dennis Peuter, Viorica Sofronie-Stokkermans
Publication date: 10 March 2020
Full work available at URL: https://arxiv.org/abs/1905.12524
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items
Symbol elimination and applications to parametric entailment problems, On invariant synthesis for parametric systems, Combination of uniform interpolants via Beth definability, Combined covers and Beth definability
Uses Software
Cites Work
- An extension of lazy abstraction with interpolation for programs with arrays
- A quantifier-elimination based heuristic for automatically generating inductive assertions for programs
- Property-directed incremental invariant generation
- Refutational theorem proving for hierarchic first-order theories
- On invariant synthesis for parametric systems
- Modular proof systems for partial functions with Evans equality
- On Interpolation and Symbol Elimination in Theory Extensions
- Decidability of inferring inductive invariants
- Obtaining Finite Local Theory Axiomatizations via Saturation
- When Is a Formula a Loop Invariant?
- Towards Complete Reasoning about Axiomatic Specifications
- Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis
- Property-Directed Inference of Universal Invariants or Proving Their Absence
- Locality Transfer: From Constrained Axiomatizations to Reachability Predicates
- Verifying CSP-OZ-DC Specifications with Complex Data Types and Timing Parameters
- Interpolation in Local Theory Extensions
- Interpolation in local theory extensions
- Deciding the Inductive Validity of ∀ ∃ * Queries
- Hierarchical Reasoning and Model Generation for the Verification of Parametric Hybrid Systems
- Interpolation and Symbol Elimination
- Loop Analysis by Quantification over Iterations
- Automated Reasoning
- Automated Deduction – CADE-20
- Automated Deduction – CADE-20
- Quantifier-free interpolation in combinations of equality interpolating theories
- Invariant Synthesis for Combined Theories
- On Local Reasoning in Verification
- On Hierarchical Reasoning in Combinations of Theories
- Hierarchical Reasoning for the Verification of Parametric Systems
- Interpolation and Symbol Elimination in Vampire
- Verification, Model Checking, and Abstract Interpretation
- Quantifiers on demand
