TY - GEN
T1 - Verified Software Units for Simple DFA Modules and Objects in C
AU - Beringer, Lennart
N1 - Publisher Copyright:
© 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.
PY - 2022
Y1 - 2022
N2 - 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.
AB - 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.
KW - Deterministic finite automata
KW - Formal verification
KW - Semantic subtyping
KW - Verified Software Toolchain
KW - Verified Software Units
UR - http://www.scopus.com/inward/record.url?scp=85142684993&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85142684993&partnerID=8YFLogxK
U2 - 10.1007/978-3-031-19756-7_14
DO - 10.1007/978-3-031-19756-7_14
M3 - Conference contribution
AN - SCOPUS:85142684993
SN - 9783031197550
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 237
EP - 258
BT - Leveraging Applications of Formal Methods, Verification and Validation. Software Engineering - 11th International Symposium, ISoLA 2022, Proceedings
A2 - Margaria, Tiziana
A2 - Steffen, Bernhard
PB - Springer Science and Business Media Deutschland GmbH
T2 - 11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2022
Y2 - 22 October 2022 through 30 October 2022
ER -