Predicate abstraction for program verification
From MaRDI portal
Recommendations
- Predicate abstraction in program verification: survey and current trends
- Transition predicate abstraction and fair termination
- Verification and falsification of programs with loops using predicate abstraction
- scientific article; zbMATH DE number 1953015
- Predicate abstraction for software verification
Cites work
- scientific article; zbMATH DE number 1670555 (Why is no real title available?)
- scientific article; zbMATH DE number 1670775 (Why is no real title available?)
- scientific article; zbMATH DE number 1693447 (Why is no real title available?)
- scientific article; zbMATH DE number 1701764 (Why is no real title available?)
- scientific article; zbMATH DE number 2102703 (Why is no real title available?)
- scientific article; zbMATH DE number 3302923 (Why is no real title available?)
- A constraint-based approach to solving games on infinite graphs
- Abstraction and abstraction refinement
- Abstractions from proofs
- An abstract interpretation framework for termination
- An axiomatic basis for computer programming
- Array Abstractions from Proofs
- Combining model checking and data-flow analysis
- Computer Aided Verification
- Counterexample-guided focus
- Lazy Abstraction with Interpolants
- Lazy abstraction
- Linear reasoning. A new form of the Herbrand-Gentzen theorem
- Low-level liquid types
- Nested interpolants
- Predicate abstraction and refinement for verifying multi-threaded programs
- Ramsey versus lexicographic termination proving
- Size-change termination and transition invariants
- Software model checking
- Static Analysis
- The ACL2 Sedan theorem proving system
- The size-change principle for program termination
- Tools and Algorithms for the Construction and Analysis of Systems
- Transition invariants and transition predicate abstraction for program termination
- Transition predicate abstraction and fair termination
- Verification, Model Checking, and Abstract Interpretation
Cited in
(44)- Model-checking structured context-free languages
- Software Verification of Hyperproperties Beyond k-Safety
- scientific article; zbMATH DE number 1953015 (Why is no real title available?)
- scientific article; zbMATH DE number 7577575 (Why is no real title available?)
- Combining Predicate Abstraction with Fixpoint Approximations
- Predicate abstraction for linked data structures
- Predicate abstraction in a program logic calculus
- Counterexample classification
- Reasoning about TSO programs using reduction and abstraction
- Verifiable certificates for predicate subtyping
- Interpolation and model checking
- Predicate abstraction and refinement for verifying multi-threaded programs
- Formal verification for C program
- NIL: learning nonlinear interpolants
- Symbolic realisation of epistemic processes
- Necessary and Sufficient Preconditions via Eager Abstraction
- Tools and Algorithms for the Construction and Analysis of Systems
- Temporal logic and fair discrete systems
- Backward symbolic execution with loop folding
- Predicate Abstraction of Programs with Non-linear Computation
- Abstraction and abstraction refinement
- Predicate abstraction and CEGAR for \(\nu \mathrm{HFL}_\mathbb{Z}\) validity checking
- Predicate extension of symbolic memory graphs for the analysis of memory safety correctness
- Complexity and Algorithms for Monomial and Clausal Predicate Abstraction
- Verification and falsification of programs with loops using predicate abstraction
- scientific article; zbMATH DE number 2102703 (Why is no real title available?)
- Constraint-Based Invariant Inference over Predicate Abstraction
- Abstract interpretation of recursive logic definitions for efficient runtime assertion checking
- SAT-Based Model Checking
- Counter-example guided program verification
- Satisfiability modulo theories
- Automatic verification of Golog programs via predicate abstraction
- Program security verification based on abstract invariants
- On height and happiness
- Tools and Algorithms for the Construction and Analysis of Systems
- Combining Model Checking and Deduction
- Structural Abstraction of Software Verification Conditions
- Symbolic execution for refuting hyperproperties
- Transition invariants and transition predicate abstraction for program termination
- Predicate Abstraction in a Program Logic Calculus
- Predicate abstraction for software verification
- Tools and Algorithms for the Construction and Analysis of Systems
- Transition predicate abstraction and fair termination
- Predicate abstraction for hyperliveness verification
Describes a project that uses
Uses Software
This page was built for publication: Predicate abstraction for program verification
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3176373)
