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.1872MaRDI 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 theories; invariant synthesis; infinite-state model checking; safety problem; backward reachability
68Q60: Specification and verification (program logics, model checking, etc.)
Related Items
SMT-based verification of data-aware processes: a model-theoretic approach, Predicate Abstraction in Program Verification: Survey and Current Trends, Verification of SMT systems with quantifiers, Synthesizing history and prophecy variables for symbolic model checking, Decision procedures for flat array properties, An extension of lazy abstraction with interpolation for programs with arrays, Multi-parameterised compositional verification of safety properties, A unifying view on SMT-based software verification, Superposition as a decision procedure for timed automata, 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, Combination of uniform interpolants via Beth definability, Parameterized model checking on the TSO weak memory model, On invariant synthesis for parametric systems, Symbolic backward reachability with effectively propositional logic. Application to security policy analysis
Uses Software
