Accurate invariant checking for programs manipulating lists and arrays with infinite data

DOI10.1007/978-3-642-33386-6_14MaRDI QIDQ4649295zbMATH OpenOpenAlexFDO

Authors Ahmed Bouajjani, Cezara Drăgoi, Constantin Enea, Mihaela Sighireanu

Publication date 21 November 2012

Published in Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-33386-6_14

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Data structures (68P05)

Recommendations

• Abstract domains for automated reasoning about list-manipulating programs with infinite data
• Compositional invariant checking for overlaid and nested linked lists
• Propositional reasoning about safety and termination of heap-manipulating programs
• Towards Model-Checking Programs with Lists
• Compositional entailment checking for a fragment of separation logic

Cited in

(7)

• A complete decision procedure for linearly compositional separation logic with data constraints
• Abstract domains for automated reasoning about list-manipulating programs with infinite data
• Counterexample validation and interpolation-based refinement for forest automata
• Verification of heap manipulating programs with ordered data by extended forest automata
• Invariant Checking for Programs with Procedure Calls
• Predicate Abstraction in Program Verification: Survey and Current Trends
• Compositional invariant checking for overlaid and nested linked lists

This page was built for publication: Accurate invariant checking for programs manipulating lists and arrays with infinite data

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