Verification of safety properties for concurrent assembly code

Concurrency, as a useful feature of many modern programming languages and systems, is generally hard to reason about. Although existing work has explored the verification of concurrent programs using high-level languages and calculi, the verification of concurrent assembly code remains an open problem, largely due to the lack of abstraction at a low-level. Nevertheless, it is sometimes necessary to reason about assembly code or machine executables so as to achieve higher assurance. In this paper, we propose a logic-based "type" system for the static verification of concurrent assembly programs, applying the "invariance proof" technique for verifying general safety properties and the "assume-guarantee" paradigm for decomposition. In particular, we introduce a notion of "local guarantee" for the thread-modular verification in a non-preemptive setting. Our system is fully mechanized. Its soundness has been verified using the Coq proof assistant. A ...

• Type: Conference
• Year: 2004
• Where: ICFP
• Authors: Dachuan Yu, Zhong Shao
• Keywords: Concurrent Assembly Programs, Coq Proof Assistant, ICFP 2004, NSF ITR Grant, Programming Languages