Predicate abstraction for software verification
From MaRDI portal
Theory of programming languages (68N15) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)
Recommendations
- Verification and falsification of programs with loops using predicate abstraction
- Predicate abstraction for program verification
- Verification, Model Checking, and Abstract Interpretation
- Tools and Algorithms for the Construction and Analysis of Systems
- Predicate Abstraction in Program Verification: Survey and Current Trends
Cited in
(35)- Higher-order quantifier elimination, counter simulations and fault-tolerant systems
- Backward symbolic execution with loop folding
- scientific article; zbMATH DE number 1630105 (Why is no real title available?)
- Predicate abstraction for linked data structures
- Computing Preconditions and Postconditions of While Loops
- Predicate abstraction for program verification
- Abstraction Refinement for Quantified Array Assertions
- Predicate Abstraction of Programs with Non-linear Computation
- Predicate Abstraction in a Program Logic Calculus
- Verifying Reference Counting Implementations
- Inferring complete initialization of arrays
- An extension of lazy abstraction with interpolation for programs with arrays
- Reuse in Software Verification by Abstract Method Calls
- Generic abstraction of dictionaries and arrays
- Loop invariants: analysis, classification, and examples
- Counterexample-guided focus
- Model Checking Software
- Tools and Algorithms for the Construction and Analysis of Systems
- Array Abstractions from Proofs
- Structural Abstraction of Software Verification Conditions
- An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures
- Non-disjunctive Numerical Domain for Array Predicate Abstraction
- Predicate abstraction in a program logic calculus
- MCMT: a model checker modulo theories
- Predicate generation for learning-based quantifier-free loop invariant inference
- Tools and Algorithms for the Construction and Analysis of Systems
- Formal Methods at the Crossroads. From Panacea to Foundational Support
- Verification, Model Checking, and Abstract Interpretation
- Mechanical inference of invariants for FOR-loops
- Invariant inference with provable complexity from the monotone theory
- Interpolation and SAT-based model checking revisited: adoption to software verification
- Lost in abstraction: monotonicity in multi-threaded programs
- Implicit semi-algebraic abstraction for polynomial dynamical systems
- \textsc{Diffy}: inductive reasoning of array programs using difference invariants
- Verification and falsification of programs with loops using predicate abstraction
This page was built for publication: Predicate abstraction for software verification
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5178906)
