Verification, Model Checking, and Abstract Interpretation

DOI10.1007/11609773zbMath1176.68116OpenAlexW2496613029MaRDI QIDQ5898633

Henny B. Sipma, Aaron R. Bradley, Zohar Manna

Publication date: 12 February 2007

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/11609773

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

RustHorn: CHC-Based Verification for Rust Programs ⋮ Splitting via Interpolants ⋮ Decision procedures for flat array properties ⋮ Adding decision procedures to SMT solvers using axioms with triggers ⋮ Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays ⋮ Dependently typed array programs don't go wrong ⋮ Satisfiability Modulo Theories ⋮ Decision Procedure for Entailment of Symbolic Heaps with Arrays ⋮ Data abstraction: a general framework to handle program verification of data structures ⋮ Symbolic automatic relations and their applications to SMT and CHC solving ⋮ A Logic-Based Framework for Reasoning about Composite Data Structures ⋮ NP satisfiability for arrays as powers ⋮ Generalized arrays for Stainless frames ⋮ Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems ⋮ Inferring complete initialization of arrays ⋮ Unnamed Item ⋮ Interpolation Results for Arrays with Length and MaxDiff ⋮ Relational abstract interpretation of arrays in assembly code ⋮ A solver for arrays with concatenation ⋮ Property Directed Reachability for Proving Absence of Concurrent Modification Errors ⋮ Modular instantiation schemes ⋮ A New Acceleration-Based Combination Framework for Array Properties ⋮ On algebraic array theories ⋮ A Decision Procedure for a Theory of Finite Sets with Finite Integer Intervals ⋮ Time warps, from algebra to algorithms ⋮ On deciding satisfiability by theorem proving with speculative inferences ⋮ An instantiation scheme for satisfiability modulo theories ⋮ A learning-based approach to synthesizing invariants for incomplete verification engines ⋮ Towards SMT Model Checking of Array-Based Systems ⋮ Decision procedures for extensions of the theory of arrays ⋮ Interpolation and amalgamation for arrays with MaxDiff ⋮ Parametrized invariance for infinite state processes ⋮ Incremental search for conflict and unit instances of quantified formulas with E-matching ⋮ Complexity of fixed-size bit-vector logics ⋮ Schemata of SMT-Problems ⋮ Predicate Pairing for program verification ⋮ Loop invariants ⋮ Inferring Loop Invariants Using Postconditions ⋮ On Hierarchical Reasoning in Combinations of Theories ⋮ Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development ⋮ Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates ⋮ Satisfiability Solving and Model Generation for Quantified First-Order Logic Formulas ⋮ Invariant Synthesis for Combined Theories ⋮ Path Feasibility Analysis for String-Manipulating Programs ⋮ On Local Reasoning in Verification ⋮ Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic ⋮ Towards Complete Reasoning about Axiomatic Specifications ⋮ Counterexample-guided prophecy for model checking modulo the theory of arrays ⋮ Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists ⋮ Improving ENIGMA-style clause selection while learning from history ⋮ On invariant synthesis for parametric systems ⋮ Algorithmic Analysis of Array-Accessing Programs ⋮ Selective Unification in (Constraint) Logic Programming* ⋮ Theory decision by decomposition ⋮ Combination of convex theories: modularity, deduction completeness, and explanation ⋮ Applications of Hierarchical Reasoning in the Verification of Complex Systems ⋮ Array theory of bounded elements and its applications