×

zbMATH — the first resource for mathematics

Formalizing single-assignment program verification: an adaptation-complete approach. (English) Zbl 1335.68044
Thiemann, Peter (ed.), Programming languages and systems. 25th European symposium on programming, ESOP 2016, held as part of the European joint conferences on theory and practice of software, ETAPS 2016, Eindhoven, The Netherlands, April 2–8, 2016. Proceedings. Berlin: Springer (ISBN 978-3-662-49497-4/pbk; 978-3-662-49498-1/ebook). Lecture Notes in Computer Science 9632, 41-67 (2016).
Summary: Deductive verification tools typically rely on the conversion of code to a single-assignment (SA) form. In this paper we formalize program verification based on the translation of while programs annotated with loop invariants into a dynamic single-assignment language with a dedicated iterating construct, and the subsequent generation of compact, indeed linear-size, verification conditions. Soundness and completeness proofs are given for the entire workflow, including the translation of annotated programs to SA form. The formalization is based on a program logic that we show to be adaptation-complete. Although this important property has not, as far as we know, been established for any existing program verification tool, we believe that adaptation-completeness is one of the major motivations for the use of SA form as an intermediate language. Our results here show that indeed this allows for the tools to achieve the maximum degree of adaptation when handling subprograms.
For the entire collection see [Zbl 1333.68019].

MSC:
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
03B70 Logic in computer science
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] America, P., de Boer, F.: Proving total correctness of recursive procedures. Inf. Comput. 84(2), 129–162 (1990) · Zbl 0699.68024 · doi:10.1016/0890-5401(90)90037-I
[2] Apt, K.R.: Ten years of Hoare’s logic: a survey - part 1. ACM Trans. Program. Lang. Syst. 3(4), 431–483 (1981) · Zbl 0471.68006 · doi:10.1145/357146.357150
[3] Barnes, J.: High Integrity Software: The SPARK Approach to Safety and Security. Addison-Wesley, Boston (2003)
[4] Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., M. Leino, K.R.: Boogie: a modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364–387. Springer, Heidelberg (2006) · Zbl 05189652 · doi:10.1007/11804192_17
[5] Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. ACM SIGSOFT Softw. Eng. Notes 31(1), 82–87 (2006) · doi:10.1145/1108768.1108813
[6] Barnett, M., M. Leino, K.R., Schulte, W.: The Spec# programming system: an overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005) · doi:10.1007/978-3-540-30569-9_3
[7] Baudin, P., Cuoq, P., Filliâtre, J.-C., Marché, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI/ISO C specification language. In: CEA LIST and INRIA (2010)
[8] Clarke, E., Kroning, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004) · Zbl 1126.68470 · doi:10.1007/978-3-540-24730-2_15
[9] Stephen, A.: Cook: soundness and completeness of an axiom system for program verification. SIAM J. Comput. 7(1), 70–90 (1978) · Zbl 0374.68009 · doi:10.1137/0207005
[10] Correnson, L., Cuoq, P., Puccetti, A., Signoles, J.: Frama-C user manual (2010). http://frama-c.com
[11] Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficiently computing static single assignment form and the control dependence graph. ACM Trans. Program. Lang. Syst. 13(4), 451–490 (1991) · doi:10.1145/115372.115320
[12] Dijkstra, E.W., Scholten, C.S.: Predicate calculus and program semantics. Springer, Scholten (1990) · Zbl 0698.68011 · doi:10.1007/978-1-4612-3228-5
[13] Filliâtre, J.-C., Paskevich, A.: Why3 – where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125–128. Springer, Heidelberg (2013) · Zbl 1435.68366 · doi:10.1007/978-3-642-37036-6_8
[14] Flanagan, C., Saxe, J.B.: Avoiding exponential explosion: generating compact verification conditions. In: Proceedings of POpPL, pp. 193–205. ACM (2001) · Zbl 1323.68372 · doi:10.1145/373243.360220
[15] Gordon, M., Collavizza, H.: Forward with Hoare. In: Roscoe, A.W., Jones, C.B., Wood, K.R. (eds.) Reflections on the Work of C.A.R. Hoare: History of Computing, pp. 101–121. Springer, London (2010) · Zbl 1215.68129 · doi:10.1007/978-1-84882-912-1_5
[16] Grigore, R., Charles, J., Fairmichael, F., Kiniry, J.: Strongest postcondition of unstructured programs. In: Proceedings of FTfJP, pp. 6:1–6:7. ACM (2009) · doi:10.1145/1557898.1557904
[17] Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969) · Zbl 0179.23105 · doi:10.1145/363235.363259
[18] Hoare, C.A.R.: Procedures and parameters: an axiomatic approach. In: Engeler, E. (ed.) Proceeedings of Symposium on Semantics of Algorithmic Languages. Lecture Notes in Mathematics, vol. 188, pp. 102–116. Springer, Heidelberg (1971) · Zbl 0221.68020 · doi:10.1007/BFb0059696
[19] Jhala, R., Majumdar, R.: Software model checking. ACM Comput. Surv. 41(4), 21 (2009) · doi:10.1145/1592434.1592438
[20] Kleymann, T.: Hoare logic and auxiliary variables. Formal Aspects Comput. 11(5), 541–566 (1999) · Zbl 0978.03026 · doi:10.1007/s001650050057
[21] Kroening, D.: Software verification. In: Biere, A., Heule, M., Van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 505–532. IOS Press, Amsterdam (2009)
[22] Rustan, K., Leino, M., Saxe, J.B., Stata, R.: Checking Java programs via guarded commands. In: Proceedings of ECOOP, pp. 110–111. Springer (1999)
[23] Rustan, K., Leino, M.: Efficient weakest preconditions. Inf. Process. Lett. 93(6), 281–288 (2005) · Zbl 1173.68563 · doi:10.1016/j.ipl.2004.10.015
[24] Loureno, C.B., Frade, M.J., Pinto, J.S.: A single-assignment translation for annotated programs. ArXiv e-prints (2016). http://arxiv.org/abs/1601.00584
[25] Marché, C., Paulin-Mohring, C., Urbain, X.: The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML. J. Logic Algebraic Program. 58(1–2), 89–106 (2004) · Zbl 1073.68678 · doi:10.1016/j.jlap.2003.07.006
[26] Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS, pp. 55–74. IEEE Computer Society (2002) · doi:10.1109/LICS.2002.1029817
[27] Vanbroekhoven, P., Janssens, G., Bruynooghe, M., Catthoor, F.: A practical dynamic single assignment transformation. ACM Trans. Des. Autom. Electron. Syst. 12(4), 40 (2007) · Zbl 05456899 · doi:10.1145/1278349.1278353
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.