Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data

DOI10.1007/978-3-642-27940-9_1zbMath1325.68058OpenAlexW1954117780MaRDI QIDQ2891398

Cezara Dragoi, Ahmed Bouajjani, Constantin Enea, Mihaela Sighireanu

Publication date: 15 June 2012

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-27940-9_1

Mathematics Subject Classification ID

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

Related Items (3)

A generic framework for heap and value analyses of object-oriented programming languages ⋮ Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists ⋮ Invariants Synthesis over a Combined Domain for Automated Program Verification

Uses Software

• Apron
• cvc3
• z3

Cites Work

• Unnamed Item
• The octagon abstract domain
• Lifting abstract interpreters to quantified logical domains
• Relational inductive shape analysis
• Shape-Value Abstraction for Verifying Linearizability
• Interprocedural Shape Analysis with Separated Heap Abstractions
• An Analysis of Permutations in Arrays
• Statically Inferring Complex Heap, Array, and Numeric Invariants
• Systematic design of program transformation frameworks by abstract interpretation
• Counterexample-guided focus
• A combination framework for tracking partition sizes
• Compositional shape analysis by means of bi-abduction
• A semantics for procedure local heaps and its abstractions
• A framework for numeric analysis of array operations
• Calling context abstraction with shapes
• Array Abstractions from Proofs
• Invariant Synthesis for Combined Theories
• Programs with Lists Are Counter Automata
• Static Analysis
• Static Analysis

This page was built for publication: Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data