TY - GEN
T1 - Verified Software Units
AU - Beringer, Lennart
N1 - Publisher Copyright:
© 2021, The Author(s).
PY - 2021
Y1 - 2021
N2 - Modularity - the partitioning of software into units of functionality that interact with each other via interfaces - has been the mainstay of software development for half a century. In case of the C language, the main mechanism for modularity is the compilation unit / header file abstraction. This paper complements programmatic modularity for C with modularity idioms for specification and verification in the context of Verifiable C, an expressive separation logic for CompCert Clight. Technical innovations include (i) abstract predicate declarations – existential packages that combine Parkinson & Bierman’s abstract predicates with their client-visible reasoning principles; (ii) residual predicates, which help enforcing data abstraction in callback-rich code; and (iii) an application to pure (Smalltalk-style) objects that connects code verification to model-level reasoning about features such as subtyping, self, inheritance, and late binding. We introduce our techniques using concrete example modules that have all been verified using the Coq proof assistant and combine to fully linked verified programs using a novel, abstraction-respecting component composition rule for Verifiable C.
AB - Modularity - the partitioning of software into units of functionality that interact with each other via interfaces - has been the mainstay of software development for half a century. In case of the C language, the main mechanism for modularity is the compilation unit / header file abstraction. This paper complements programmatic modularity for C with modularity idioms for specification and verification in the context of Verifiable C, an expressive separation logic for CompCert Clight. Technical innovations include (i) abstract predicate declarations – existential packages that combine Parkinson & Bierman’s abstract predicates with their client-visible reasoning principles; (ii) residual predicates, which help enforcing data abstraction in callback-rich code; and (iii) an application to pure (Smalltalk-style) objects that connects code verification to model-level reasoning about features such as subtyping, self, inheritance, and late binding. We introduce our techniques using concrete example modules that have all been verified using the Coq proof assistant and combine to fully linked verified programs using a novel, abstraction-respecting component composition rule for Verifiable C.
KW - Abstract Predicate Declaration
KW - Positive Subtyping
KW - Residual Predicate
KW - Verified Software Toolchain
KW - Verified Software Unit
UR - http://www.scopus.com/inward/record.url?scp=85105016383&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85105016383&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-72019-3_5
DO - 10.1007/978-3-030-72019-3_5
M3 - Conference contribution
AN - SCOPUS:85105016383
SN - 9783030720186
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 118
EP - 147
BT - Programming Languages and Systems - 30th European Symposium on Programming, ESOP 2021 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Proceedings
A2 - Yoshida, Nobuko
PB - Springer Science and Business Media Deutschland GmbH
T2 - 30th European Symposium on Programming, ESOP 2021 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021
Y2 - 27 March 2021 through 1 April 2021
ER -