Predicate abstraction for software verification

DOI10.1145/503272.503291zbMath1323.68371OpenAlexW1972085995MaRDI QIDQ5178906

Cormac Flanagan, Shaz Qadeer

Publication date: 17 March 2015

Published in: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/503272.503291

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Theory of programming languages (68N15) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (18)

Implicit semi-algebraic abstraction for polynomial dynamical systems ⋮ \textsc{Diffy}: inductive reasoning of array programs using difference invariants ⋮ Backward symbolic execution with loop folding ⋮ Mechanical inference of invariants for FOR-loops ⋮ Inferring complete initialization of arrays ⋮ Invariant inference with provable complexity from the monotone theory ⋮ An extension of lazy abstraction with interpolation for programs with arrays ⋮ Generic Abstraction of Dictionaries and Arrays ⋮ Predicate abstraction in a program logic calculus ⋮ MCMT: A Model Checker Modulo Theories ⋮ Predicate Abstraction in a Program Logic Calculus ⋮ Higher-order quantifier elimination, counter simulations and fault-tolerant systems ⋮ Lost in abstraction: monotonicity in multi-threaded programs ⋮ An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures ⋮ Verifying Reference Counting Implementations ⋮ Non-disjunctive Numerical Domain for Array Predicate Abstraction ⋮ Abstraction Refinement for Quantified Array Assertions ⋮ Computing Preconditions and Postconditions of While Loops

This page was built for publication: Predicate abstraction for software verification