A relational approach to interprocedural shape analysis

DOI10.1007/978-3-540-27864-1_19MaRDI QIDQ5466564zbMATH OpenOpenAlexFDO

Authors Bertrand Jeannet, Alexey Loginov, Mooly Sagiv, Thomas Reps

Publication date 24 August 2005

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

Full work available at URL https://doi.org/10.1007/b99688, http://digital.library.wisc.edu/1793/60398

Mathematics Subject Classification ID

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

Recommendations

• Interprocedural shape analysis for recursive programs
• Static Analysis
• Interprocedural Shape Analysis with Separated Heap Abstractions
• Abstracting call-stacks for interprocedural verification of imperative programs
• Interprocedural shape analysis for effectively cutpoint-free programs

Cited in

(23)

• A relational shape abstract domain
• Interprocedural shape analysis using separation logic-based transformer summaries
• Disjunctive relational abstract interpretation for interprocedural program analysis
• Fragment abstraction for concurrent shape analysis
• Interprocedural shape analysis for recursive programs
• A relational framework for higher-order shape analysis
• 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
• Typed intermediate languages for shape analysis
• Relational inductive shape analysis
• Scalable Shape Analysis for Systems Code
• Interprocedural Shape Analysis with Separated Heap Abstractions
• Automatically analyzing inductive properties for recursive data structures
• Interprocedural shape analysis for effectively cutpoint-free programs
• A semantics for procedure local heaps and its abstractions
• Abstracting call-stacks for interprocedural verification of imperative programs
• Calling context abstraction with shapes
• Static Analysis
• Verifying pointer safety for programs with unknown calls
• Lifting numeric relational domains to algebraic data types
• An input-output relational domain for algebraic data types and functional arrays
• Summarization for termination: No return!

Describes a project that uses

Uses Software

• Octagon
• Smallfoot

This page was built for publication: A relational approach to interprocedural shape analysis

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