Verification of safety properties for concurrent assembly code

DOI10.1145/1016850.1016875MaRDI QIDQ5178035zbMATH OpenOpenAlexFDO

Authors Dachuan Yu, Zhong Shao

Publication date 9 March 2015

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

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

zbMATH Keywords

assemblyconcurrencylocal guarantee

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

• Modular verification of concurrent assembly code with dynamic thread creation and termination
• Modular verification of SPARCv8 code
• Verification of concurrent systems with VerCors
• Verifying branch-free assembly code in Why3
• A Coq library for verification of concurrent programs

Cited in

(10)

• Local proofs for global safety properties
• Verifying branch-free assembly code in Why3
• Safe functional systems through integrity types and verified assembly
• A Coq library for verification of concurrent programs
• Modular verification of concurrent assembly code with dynamic thread creation and termination
• A verifiable low-level concurrent programming model based on colored Petri nets
• Formal verification of concurrent programs with Read-write locks
• scientific article; zbMATH DE number 522852 (Why is no real title available?)
• Verification of concurrent systems with VerCors
• Modular verification of SPARCv8 code

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Verification of safety properties for concurrent assembly code

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