Array Abstractions from Proofs
From MaRDI portal
Publication:5429322
DOI10.1007/978-3-540-73368-3_23zbMath1135.68474OpenAlexW171295454MaRDI QIDQ5429322
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
Related Items
Verifying Array Manipulating Programs with Full-Program Induction ⋮ Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data ⋮ Decision procedures for flat array properties ⋮ \textsc{Diffy}: inductive reasoning of array programs using difference invariants ⋮ Abstraction and Abstraction Refinement ⋮ Predicate Abstraction for Program Verification ⋮ A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis ⋮ Predicate Abstraction in Program Verification: Survey and Current Trends ⋮ An extension of lazy abstraction with interpolation for programs with arrays ⋮ An array content static analysis based on non-contiguous partitions ⋮ Automatically inferring loop invariants via algorithmic learning ⋮ Interpolation and Symbol Elimination in Vampire ⋮ Static Contract Checking with Abstract Interpretation ⋮ Verifying Reference Counting Implementations ⋮ Efficient Interpolant Generation in Satisfiability Modulo Theories ⋮ Non-disjunctive Numerical Domain for Array Predicate Abstraction ⋮ Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference ⋮ Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists ⋮ Abstraction Refinement for Quantified Array Assertions
This page was built for publication: Array Abstractions from Proofs
