From shape analysis to termination analysis in linear time

DOI10.1007/978-3-319-41528-4_23MaRDI QIDQ4633546zbMATH OpenOpenAlexFDO

Authors Roman Manevich, Boris Dogadov, Noam Rinetzky

Publication date 3 May 2019

Published in Computer Aided Verification (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-41528-4_23

Mathematics Subject Classification ID

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

Recommendations

• Automatic Termination Proofs for Programs with Shape-Shifting Heaps
• Heap Assumptions on Demand
• scientific article; zbMATH DE number 1693492
• A Shape Analysis for Non-linear Data Structures
• Cyclic proofs of program termination in separation logic

Cited in

(4)

• Temporal prophecy for proving temporal properties of infinite-state systems
• Inference of field-sensitive reachability and cyclicity
• Heap Assumptions on Demand
• Automatic Termination Proofs for Programs with Shape-Shifting Heaps

This page was built for publication: From shape analysis to termination analysis in linear time

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