Mechanized, Compositional Verification of Low-Level Code
Mechanized, Compositional Verification of Low-Level Code
复制标题
低级代码的机械化、组合验证
DOI：
10.1007/978-3-319-06200-6_8
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Nils Jähnig
中科院分区：
文献类型：
--
作者：
Björn Bartels;Nils Jähnig
对于许多安全关键型系统来说，除了功能正确性之外，终端属性尤其重要。理想情况下，这种性质不仅适用于系统的高级表示，也适用于低级表示。因此，本文针对可能存在不确定性的低级语言，提出了一种组合语义学和相关的证明演算。该演算有助于对用低级语言给出的程序表示的完全正确性证明。我们通过使用定理证明者Isabelle/HOL将整个理论机械化，并利用证明者机制来构建基础良好的关系，来处理此类证明所固有的复杂性。
For many safety-critical systems besides functional correctness, termination properties are especially important. Ideally, such properties are not only established for high-level representations of a system, but also for low-level representations.In this paper, we therefore present a compositional semantics and a related proof calculus for possibly non-deterministic low-level languages. The calculus facilitates total correctness proofs about program representations given in a low-level language. We cope with the complexity inherent to such proofs by mechanizing the entire theory using the theorem prover Isabelle/HOL and exploiting the provers mechanisms for constructing well-founded relations.
登录
查看更多内容
DOI：
--
发表时间：
2006
期刊：
SOS@ICALP
影响因子：
--
作者：
Ando Saabas;Tarmo Uustalu
通讯作者：
Tarmo Uustalu
DOI：
10.1016/0304-3975(83)90009-9
发表时间：
1983
期刊：
Theor. Comput. Sci.
影响因子：
--
作者：
E. Olderog
通讯作者：
E. Olderog
递归过程和无界非确定性的霍尔逻辑
DOI：
--
发表时间：
2002
期刊：
Annual Conference for Computer Science Logic
影响因子：
--
作者：
T. Nipkow
通讯作者：
T. Nipkow
理论计算机科学的未来会怎样？
DOI：
--
发表时间：
1997
期刊：
Theory and Practice of Software Development
影响因子：
--
作者：
Donald Sannella
通讯作者：
Donald Sannella
DOI：
--
发表时间：
1997
期刊：
Theory and Practice of Software Development
影响因子：
--
作者：
T. Schreiber
通讯作者：
T. Schreiber