Verified Software Units
Verified Software Units
复制标题
经过验证的软件单元
DOI：
10.1007/978-3-030-72019-3_5
复制
发表时间：
2021-03-23
期刊：
影响因子：
--
通讯作者：
Beringer L
中科院分区：
文献类型：
--
作者：
Beringer L
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.
登录
查看更多内容
影响因子：
1
作者：
Bruce, KB;Cardelli, L;Pierce, BC
通讯作者：
Pierce, BC
影响因子：
2.5
作者：
Banerjee, Anindya;Naumann, David A.
通讯作者：
Naumann, David A.
影响因子：
1.1
作者：
Besson, Frederic;Jensen, Thomas;Pichardie, David
通讯作者：
Pichardie, David
DOI：
10.1145/1709093.1709094
发表时间：
2010-03-01
影响因子：
1.3
作者：
Ahmed, Amal;Appel, Andrew W.;Wang, Daniel C.
通讯作者：
Wang, Daniel C.
影响因子：
22.7
作者：
Hawblitzel, Chris;Howell, Jon;Zill, Brian
通讯作者：
Zill, Brian