Abstraction Refinement for Quantified Array Assertions

DOI10.1007/978-3-642-03237-0_3zbMath1248.68151OpenAlexW1951162889MaRDI QIDQ3392917

Andreas Podelski, Mohamed Nassim Seghir, Thomas Wies

Publication date: 18 August 2009

Published in: Static Analysis (Search for Journal in Brave)

Full work available at URL: https://www.pure.ed.ac.uk/ws/files/19313277/Seghir_Podelski_ET_AL_2009_Abstraction_Refinement_for_Quantified_Array_Assertions.pdf

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (5)

An extension of lazy abstraction with interpolation for programs with arrays ⋮ An array content static analysis based on non-contiguous partitions ⋮ Generic Abstraction of Dictionaries and Arrays ⋮ An Assume Guarantee Approach for Checking Quantified Array Assertions ⋮ Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists

Uses Software

• ACSAR
• SLAM
• ARMC

Cites Work

• Unnamed Item
• Unnamed Item
• Lifting abstract interpreters to quantified logical domains
• Abstractions from proofs
• Lazy abstraction
• Predicate abstraction for software verification
• A framework for numeric analysis of array operations
• Logical characterizations of heap abstractions
• Computer Aided Verification
• Computer Aided Verification
• Array Abstractions from Proofs
• Invariant Synthesis for Combined Theories
• Quantified Invariant Generation Using an Interpolating Saturation Prover
• Verification, Model Checking, and Abstract Interpretation
• Static Analysis
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: Abstraction Refinement for Quantified Array Assertions