Array Abstractions from Proofs

DOI10.1007/978-3-540-73368-3_23zbMATH Open1135.68474OpenAlexW171295454MaRDI QIDQ5429322FDOQ5429322

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

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

Mathematics Subject Classification ID

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

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
• Automatically inferring loop invariants via algorithmic learning
• Abstraction Refinement for Quantified Array Assertions
• The map equality domain
• Decision procedures for flat array properties
• Non-disjunctive Numerical Domain for Array Predicate Abstraction
• Predicate abstraction for program verification
• Efficient Interpolant Generation in Satisfiability Modulo Theories
• An extension of lazy abstraction with interpolation for programs with arrays
• 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
• Title not available (Why is that?)
• 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)