Formal Modeling and Verification of Low-Level Software Programs

Process-algebraic formalisms offer convenient mechanisms for specifying and analyzing concurrent system behavior on an abstract level, but the high level of abstraction comes at the cost of introducing a semantic gap between the actual implementation and its specification. To bridge this gap, we semi-automatically synthesize a process-specific system model from its implementation-level description. In this paper, we show how the correctness of the synthesis procedure can be shown for a given instance by establishing a bisimulation relation between the process-specific model and its low-level system model. This enables us to reason about a system on an abstract level that faithfully captures the semantics of the low-level implementation.