Interprocedural shape analysis using separation logic-based transformer summaries

DOI10.1007/978-3-030-65474-0_12MaRDI QIDQ2233537zbMATH OpenOpenAlexFDO

Authors Hugo Illous, Matthieu Lemerre, Xavier Rival

Publication date 18 October 2021

Full work available at URL https://hal.inria.fr/hal-03081558/file/sas.pdf

Mathematics Subject Classification ID

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

Recommendations

• Interprocedural Shape Analysis with Separated Heap Abstractions
• Static Analysis
• Static Analysis
• Interprocedural shape analysis for effectively cutpoint-free programs
• Calling context abstraction with shapes

Cites work

• scientific article; zbMATH DE number 1693492 (Why is no real title available?)
• A semantics for procedure local heaps and its abstractions
• Axiomatic approach to total correctness of programs
• Bottom-Up Shape Analysis
• Calling context abstraction with shapes
• Precise interprocedural analysis through linear algebra
• Static Analysis
• Static Analysis
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(3)

• Static Analysis
• Lifting numeric relational domains to algebraic data types
• A relational shape abstract domain

This page was built for publication: Interprocedural shape analysis using separation logic-based transformer summaries

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