Verification of safety properties for concurrent assembly code

14 years 5 months ago
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 ...
Dachuan Yu, Zhong Shao
Added 13 Dec 2009
Updated 13 Dec 2009
Type Conference
Year 2004
Where ICFP
Authors Dachuan Yu, Zhong Shao
Comments (0)