An extension of lazy abstraction with interpolation for programs with arrays
From MaRDI portal
Publication:479820
DOI10.1007/s10703-014-0209-9zbMath1317.68107OpenAlexW2140566181MaRDI QIDQ479820
Roberto Bruttomesso, Francesco Alberti, Natasha Sharygina, Silvio Ranise, Silvio Ghilardi
Publication date: 5 December 2014
Published in: Formal Methods in System Design (Search for Journal in Brave)
Full work available at URL: http://doc.rero.ch/record/326403/files/10703_2014_Article_209.pdf
Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (6)
Decision procedures for flat array properties ⋮ A unifying view on SMT-based software verification ⋮ Efficient strategies for CEGAR-based model checking ⋮ SMT-based verification of data-aware processes: a model-theoretic approach ⋮ Interpolation and amalgamation for arrays with MaxDiff ⋮ On invariant synthesis for parametric systems
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The octagon abstract domain
- The octahedron abstract domain
- Solving quantified verification conditions using satisfiability modulo theories
- Verifying programs with unreliable channels
- Quantifier-Free Interpolation of a Theory of Arrays
- Lazy Abstraction with Interpolants for Arrays
- From Strong Amalgamability to Modularity of Quantifier-Free Interpolation
- SMT-Based Array Invariant Generation
- Static Contract Checking with Abstract Interpretation
- Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis
- Automated Termination in Model Checking Modulo Theories
- Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
- Abstraction Refinement for Quantified Array Assertions
- Abstractions from proofs
- Fluid Updates: Beyond Strong vs. Weak Updates
- Inferring Loop Invariants Using Postconditions
- Efficient E-Matching for SMT Solvers
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Simplification by Cooperating Decision Procedures
- Lazy abstraction
- Predicate abstraction for software verification
- Light-Weight SMT-based Model Checking
- A framework for numeric analysis of array operations
- Connecting many-sorted theories
- Tools and Algorithms for the Construction and Analysis of Systems
- Computer Aided Verification
- The MathSAT5 SMT Solver
- A parametric segmentation functor for fully automatic and scalable array content analysis
- Array Abstractions from Proofs
- Invariant Synthesis for Combined Theories
- Is Lazy Abstraction a Decision Procedure for Broadcast Protocols?
- Quantified Invariant Generation Using an Interpolating Saturation Prover
- MCMT: A Model Checker Modulo Theories
- Interpolation and Symbol Elimination in Vampire
- An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic
- Lazy Abstraction with Interpolants
- Abstraction Refinement of Linear Programs with Arrays
- Static Analysis
- Tools and Algorithms for the Construction and Analysis of Systems
- Verification, Model Checking, and Abstract Interpretation
This page was built for publication: An extension of lazy abstraction with interpolation for programs with arrays
