Array Abstractions from Proofs

DOI10.1007/978-3-540-73368-3_23MaRDI QIDQ5429322zbMATH OpenOpenAlexFDO

Authors Ranjit Jhala, K. L. McMillan

Publication date 29 November 2007

Published in Computer Aided Verification (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-73368-3_23

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Predicate abstraction for software verification
• Artificial Intelligence and Symbolic Computation
• Lazy abstraction with interpolants for arrays
• Abstraction Refinement for Quantified Array Assertions
• Abstractions from proofs

Cited in

(23)

• Verifying array manipulating programs with full-program induction
• Verifying Reference Counting Implementations
• \textsc{Diffy}: inductive reasoning of array programs using difference invariants
• Abstraction Refinement for Quantified Array Assertions
• Automatically inferring loop invariants via algorithmic learning
• Decision procedures for flat array properties
• The map equality domain
• An extension of lazy abstraction with interpolation for programs with arrays
• Predicate abstraction for program verification
• Non-disjunctive Numerical Domain for Array Predicate Abstraction
• Efficient Interpolant Generation in Satisfiability Modulo Theories
• Array abstraction with symbolic pivots
• Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference
• Abstraction and abstraction refinement
• Static contract checking with abstract interpretation
• Abstract domains for automated reasoning about list-manipulating programs with infinite data
• Interpolation and symbol elimination in Vampire
• Predicate Abstraction in Program Verification: Survey and Current Trends
• scientific article; zbMATH DE number 6687732 (Why is no real title available?)
• Permission inference for array programs
• A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis
• Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists
• An array content static analysis based on non-contiguous partitions

This page was built for publication: Array Abstractions from Proofs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5429322)