Verified Software Units for Simple DFA Modules and Objects in C.

Finite state machines occur ubiquitously in modern software, often in the form of C code that is synthesized from higher-level descriptions. To explore how the resulting code bases can be integrated into foundational verification infrastructures, we present formal specifications and machine-checked proofs of DFA representations using VST, a higher-order separation logic for C implemented in the Coq proof assistant. Paying particular attention to modularity and API-level representation hiding, we consider statically linked modules as well as object-inspired programming styles. Exploiting the abstraction capabilities of a recent VST enhancement, Verified Software Units (VSU), we complement separate compilation by separate verification and obtain instances of behavioral subtyping as separation logic entailments between suitable object representation predicates.