Verifying safety properties of concurrent Java programs using 3-valued logic

DOI10.1145/360204.360206MaRDI QIDQ5178871zbMATH OpenOpenAlexFDO

Authors Eran Yahav

Publication date 17 March 2015

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

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

Mathematics Subject Classification ID

Theory of programming languages (68N15) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Safety and Liveness in Concurrent Pointer Programs
• A tool-supported proof system for multithreaded Java.
• Property Directed Reachability for Proving Absence of Concurrent Modification Errors
• An integrated specification and verification technique for highly concurrent data structures
• An assertion-based proof system for multithreaded Java

Cited in

(11)

• Model checking dynamic pushdown networks
• Verification of Boolean programs with unbounded thread creation
• Verification of Java programs with interacting analysis plugins
• Verifying Reference Counting Implementations
• A model checking-based approach for security policy verification of mobile systems
• A dynamic logic for deductive verification of multi-threaded programs
• Model-checking view-based partial specifications
• The Spotlight Principle
• Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems
• Modular verification of multithreaded programs
• Translating Java for multiple model checkers: The Bandera back-end

This page was built for publication: Verifying safety properties of concurrent Java programs using 3-valued logic

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