Abstracting call-stacks for interprocedural verification of imperative programs

DOI10.1007/978-3-540-27815-3_22MaRDI QIDQ5312985zbMATH OpenOpenAlexFDO

Authors Bertrand Jeannet, Wendelin Serwe

Publication date 25 August 2005

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

Full work available at URL https://doi.org/10.1007/b98770

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• A relational approach to interprocedural shape analysis
• Summary-based inter-procedural analysis via modular trace refinement
• Calling context abstraction with shapes
• Integrated approach to analysis and verification of imperative programs
• Abstract interpretation with a theorem prover

Cited in

(8)

• Summary-based inter-procedural analysis via modular trace refinement
• Integrated approach to analysis and verification of imperative programs
• Precise interprocedural analysis in the presence of pointers to the stack
• scientific article; zbMATH DE number 1822434 (Why is no real title available?)
• Model Checking Recursive Programs with Exact Predicate Abstraction
• A semantics for procedure local heaps and its abstractions
• Calling context abstraction with shapes
• A relational approach to interprocedural shape analysis

Describes a project that uses

Uses Software

• Octagon

This page was built for publication: Abstracting call-stacks for interprocedural verification of imperative programs

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