Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis
From MaRDI portal
Publication:3081445
DOI10.2168/LMCS-6(4:10)2010zbMath1213.68379arXiv1010.1872OpenAlexW3104749005MaRDI QIDQ3081445
Silvio Ghilardi, Silvio Ranise
Publication date: 8 March 2011
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1010.1872
satisfiability modulo theoriesinvariant synthesisinfinite-state model checkingsafety problembackward reachability
Related Items (16)
Decision procedures for flat array properties ⋮ Verification of SMT systems with quantifiers ⋮ Synthesizing history and prophecy variables for symbolic model checking ⋮ A unifying view on SMT-based software verification ⋮ Superposition as a decision procedure for timed automata ⋮ Parameterized model checking on the TSO weak memory model ⋮ Symbolic backward reachability with effectively propositional logic. Application to security policy analysis ⋮ Predicate Abstraction in Program Verification: Survey and Current Trends ⋮ SMT-based verification of data-aware processes: a model-theoretic approach ⋮ An extension of lazy abstraction with interpolation for programs with arrays ⋮ Multi-parameterised compositional verification of safety properties ⋮ Formal specification and verification of dynamic parametrized architectures ⋮ Higher-order quantifier elimination, counter simulations and fault-tolerant systems ⋮ Universal invariant checking of parametric systems with quantifier-free SMT reasoning ⋮ On invariant synthesis for parametric systems ⋮ Combination of uniform interpolants via Beth definability
Uses Software
This page was built for publication: Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis
