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

DOI10.1145/1086365.1086399zbMATH Open1302.68088OpenAlexW2141260727MaRDI QIDQ2936788FDOQ2936788

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

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

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)

Cited In (5)

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

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)