Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis

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

zbMATH Keywords

satisfiability modulo theoriesinvariant synthesisinfinite-state model checkingsafety problembackward reachability

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

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

• SMT-LIB
• HyTech
• Mcmt

This page was built for publication: Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis