C program verification in SPECTRUM multilanguage system
Tóm tắt
An extendable multilanguage analysis and verification system SPECTRUM is presented; this system is being developed in the framework of the project SPECTRUM. The prospects of the application of this system are demonstrated, as exemplified by the verification of C programs. The project SPECTRUM is aimed at the creation of a new integrated approach to the verification of imperative programs that makes it possible to integrate, unify, and combine methods and approaches for verification of imperative programs and accumulate and apply information about these programs. The specific feature of this approach is the application of a specialized executable specification language Atoment for the development of program verification tools; this language makes it possible to represent methods and approaches for verification and data for them (program models, annotations, logical formulae) in a unified format. The C component of the SPECTRUM system uses a two-level C program verification method. This method is a good illustration of the integrated approach, since it provides complex verification of C programs based on a combination of the operational, axiomatic, and transformational approaches.
Tài liệu tham khảo
Anureev, I.S., Maryasov, I.V., and Nepomniaschy, V.A., C-Program Verification Based on the Mixed Axiomatic Semantics, Modelir. Analiz Inform. Sistem, 2010, vol. 17, no. 3, pp. 5–28.
Nepomniaschy, V.A., Anureev, I.S., Mikhailov, I.N., and Promskii, A.V., Towards Verification of C Programs: Axiomatic Semantics of the C-kernel Language, Program. Comput. Software 2003, vol. 29, no. 6, pp. 338–350].
Nepomniaschy, V.A., Anureev, I.S., Mikhailov, I.N., and Promsky, A.V., Verification-Oriented C-Light Language, in Sistemnaya informatika: Sb. nauch. tr (System Informatics. Collection of Scientific Papers), Novosibirsk: Sib. Otd. Ross. Akad. Nauk, 2004, no. 9.
Nepomniaschy, V.A., Anureev, I.S., Promsky, A.V., and Dubranovsky, I.V., Towards Verification of C# Programs: A Three-Level Approach, Program. Comput. Software, 2006, vol. 32, no. 4, pp. 190–202].
Anureev, I.S., A Three-Stage Method of C Program Verification, Joint NCC&IIS Bulletin, Series Computer Science, 2008, vol. 28, pp. 1–29.
Alkassar, E., Hillebrand, M.A., Leinenbach, D., Schirmer, N.W., and Starostin, A., The Verisoft Approach to System Verification, Proc. Conf. on Verified Software: Theories, Tools and Experiments (VSTTE), 2008, vol. 5295, pp. 1–29.
Cohen, E., Dahlweid, M., Hillebrand, M.A., Leinenbach, D., Moskal, M., Santen T., Schulte W., and Tobies, S., VCC: A Practical System for Verifying Concurrent C, Proc. TPHOLs 2009, Lect. Notes Comput. Sci., 2009, vol. 5674, pp. 23–42.
Filliátre, J.C. and Marché, C., Multi-Prover Verification of C Programs, Proc. ICFEM, 2004, pp. 15–29.
Jacobs, B. and Kiniry, J.L., and Warmer, M., Java Program Verification Challenges, Proc. FMCO 2002, Lect. Notes Comput. Sci., 2003, vol. 2852, pp. 202–219.
Promsky, A.V., Towards C-Light Program Verification: Overcoming the Obstacles, Proc. International Workshop on Program Understanding, Altai Mountains, Russia, 2009, pp. 53–63.