Abstract:


A Verification Approach for System-Level Concurrent Programs


Matthias Daum and Jan Dörrenbächer and Mareike Schmidt 
and Burkhart Wolff




Though the verification of operating systems is an active 
research field, a verification method is still missing that 
provides both, the proximity to practically used programming 
languages such as C and a realistic model of concurrency, 
i.e. a model that copes with the granularity of atomic 
operations actually used in a target machine.Our approach 
serves as the foundation for the verification of concurrent 
programs in C0 – a C fragment enriched by kernel communication 
primitives – in a Hoare-Logic. C0 is compiled by a verified 
compiler into assembly code representing a cooperative 
concurrent transition system. For the latter, it is shown 
that it can actually be executed in a true concurrent way 
reflecting the C0 semantics.