Developing a self-applicable verification system. Theory and practice

被引：2

作者：

Kondratyev D.A. ^{[1
]}

Promsky A.V. ^{[2
]}

机构：

[1] Novosibirsk State University, ul. Pirogova 2, Novosibirsk

[2] Ershov Institute of Informatics Systems SB RAS, pr. Academika Lavrent’eva 6, Novosibirsk

来源：

Automatic Control and Computer Sciences | 2015年 / 49卷 / 07期

基金：

俄罗斯基础研究基金会;

关键词：

axiomatic semantics; MetaVCG; specification; the C-light language; verification; verification condition;

D O I：

10.3103/S0146411615070123

中图分类号：

学科分类号：

摘要：

Compared with traditional testing, the deductive verification represents a more formal way to establish the program correctness. However, can we be sure that the verification system itself is correct? The theoretical foundations of Hoare logic were examined in classical works, and some soundness/completeness theorems are well known. Nevertheless, we practically are not aware of implementations of those theoretical methods subjected to anything more than testing. In other words, our ultimate goal is a verification system that can be self-applicable (at least partially). In our recent studies, we applied the MetaVCG approach in order to make such a task more feasible. © 2015, Allerton Press, Inc.

引用

页码：445 / 452

页数：7

共 10 条

[1]

Apt K.R., Olderog E.R., Verification of Sequential and Concurrent Programs, Berlin etc.: Springer, (1991)

[2]

Cohen E., Dahlweid M., Hillebrand M.A., Leinenbach D., Moskal M., Santen T., Schulte W., Tobies S., VCC: A practical system for verifying concurrent C, Proc. TPHOLs 2009, LNCS, 5674, pp. 23-42, (2009)

[3]

Filliatre J.C., Marche C., Multi-prover verification of C programs, Proc. ICFEM 2004, LNCS, 3308, pp. 15-29, (2004)

[4]

Maryasov I.V., Nepomnyaschy V.A., Promsky A.V., Kondratyev D.A., Automatic C program verification based on mixed axiomatic semantics, Proc. Fourth Workshop “Program Semantics, Specification and Verification: Theory and Applications,” Yekaterinburg, pp. 50-59, (2013)

[5]

Moriconi M., Schwartz R.L., Automatic construction of verification condition generators from Hoare logics, Lect. Notes Comput. Sci., 115, pp. 363-377, (1981)

[6]

Nepomnyaschy V.A., Anureev I.S., Mikhaylov I.N., Promsky A.V., Verification oriented language C-light, Sistemnaya informatika: Sb. nauch. tr., 9, pp. 51-134, (2004)

[7]

Norrish M., C formalised in HOL, PhD, (1998)

[8]

von Oheimb D., Hoare logic for Java in Isabelle/HOL, Concurrency Comput.: Pract. Exper., 13, 13, pp. 1173-1214, (2001)

[9]

Promsky A.V., C program verification: Verification condition explanation and standard library, Autom. Control Comput. Sci., 46, 7, pp. 394-401, (2012)

[10]

Promsky A.V., Experiments on self-applicability in the C-light verification system, Bull. Nov. Comp. Center, Comp. Sci., 35, pp. 85-99, (2013)

← 1 →