Verifying Temporal Heap Properties Specified via Evolution Logic

DOI10.1093/JIGPAL/JZL009MaRDI QIDQ3424121zbMATH OpenOpenAlexFDO

Authors

Publication date 15 February 2007

Published in Logic Journal of the IGPL (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1093/jigpal/jzl009

zbMATH Keywords

abstract interpretationfirst-order logictemporal logicverification

Mathematics Subject Classification ID

Temporal logic (03B44) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 1956555
• Using unified model checking to verify heaps
• Verify heaps via unified model checking
• scientific article; zbMATH DE number 7149819
• Establishing local temporal heap safety properties with applications to compile-time memory management

Cited in

(9)

• Kleene's Logic with equality
• Verify heaps via unified model checking
• Establishing local temporal heap safety properties with applications to compile-time memory management
• Using unified model checking to verify heaps
• scientific article; zbMATH DE number 1956555 (Why is no real title available?)
• scientific article; zbMATH DE number 2090863 (Why is no real title available?)
• Automatically verifying temporal properties of pointer programs with cyclic proof
• A presheaf semantics for quantified temporal logics
• A framework for the verification of infinite-state graph transformation systems

This page was built for publication: Verifying Temporal Heap Properties Specified via Evolution Logic

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