Enhancing modular OO verification with separation logic

DOI10.1145/1328438.1328452MaRDI QIDQ3189829zbMATH OpenOpenAlexWikidataFDO

Authors Wei-Ngan Chin, Cristina David, Huu Hai Nguyen, Shengchao Qin

Publication date 12 September 2014

Published in Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/1328438.1328452

zbMATH Keywords

automated verificationenhanced subsumptionlossless castingseparation logicstatic and dynamic specifications

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Separation logic, abstraction and inheritance
• Specification and verification of object-oriented programs using supertype abstraction
• Specification and verification of invariants by exploiting layers in OO designs
• Modular specification and verification of object-oriented programs
• Modular specification and verification of object-oriented programs

Cited in

(14)

• Specification and verification of object-oriented programs using supertype abstraction
• Bunched logics displayed
• Automated repair of heap-manipulating programs using deductive synthesis
• Certificates and Separation Logic
• A unified display proof theory for bunched logic
• Separation logic, abstraction and inheritance
• Automatic Parallelization and Optimization of Programs by Proof Rewriting
• Incremental Reasoning for Multiple Inheritance
• Separation Logic for Multiple Inheritance
• Incremental reasoning with lazy behavioral subtyping for multiple inheritance
• Separation Logic Contracts for a Java-Like Language with Fork/Join
• Linear quantifier elimination as an abstract decision procedure
• Modular specification and verification of object-oriented programs
• Lazy behavioral subtyping

This page was built for publication: Enhancing modular OO verification with separation logic

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