Modular verification of concurrent assembly code with dynamic thread creation and termination

DOI10.1145/1086365.1086399MaRDI QIDQ2936788zbMATH OpenOpenAlexFDO

Authors Xinyu Feng, Zhong Shao

Publication date 6 January 2015

Published in Proceedings of the tenth ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)

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

zbMATH Keywords

rely-guaranteeproof-carrying codeconcurrency verificationdynamic thread creation

Mathematics Subject Classification ID

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

Recommendations

• Verification of safety properties for concurrent assembly code
• scientific article; zbMATH DE number 2110618
• scientific article; zbMATH DE number 2163030
• A syntactic approach to foundational proof-carrying code
• scientific article; zbMATH DE number 2090287

Cited in

(5)

• Certifying low-level programs with hardware interrupts and preemptive threads
• Modular verification of SPARCv8 code
• A shared-variable concurrency analysis of multi-threaded object-oriented programs
• Formal verification of concurrent programs with Read-write locks
• Verification of safety properties for concurrent assembly code

This page was built for publication: Modular verification of concurrent assembly code with dynamic thread creation and termination

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