zbMATH — the first resource for mathematics

A generic intermediate representation for verification condition generation. (English) Zbl 06539456
Falaschi, Moreno (ed.), Logic-based program synthesis and transformation. 25th international symposium, LOPSTR 2015, Siena, Italy, July 13–15, 2015. Revised selected papers. Cham: Springer (ISBN 978-3-319-27435-5/pbk; 978-3-319-27436-2/ebook). Lecture Notes in Computer Science 9527, 227-243 (2015).
Summary: As part of a platform for computer-assisted verification, we present an intermediate representation of programs that is both language independent and appropriate for the generation of verification conditions. We show how many imperative and functional languages can be translated to this generic intermediate representation, and how the generated conditions reflect the axiomatic semantics of the original program. At this representation level, loop invariants and preconditions of recursive functions belonging to the original program are represented by assertions placed at certain edges of a directed graph.
The paper defines the generic representation, sketches the transformation algorithms, and describes how the places where the invariants should be placed are computed. Assuming that, either manually or assisted by the platform, the invariants have been settled, it is shown how the verification conditions are generated. A running example illustrates the process.
For the entire collection see [Zbl 1326.68017].
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
CVC4; GHC; KeY; OCaml; Why3; WhyML; z3
Full Text: DOI
[1] Ahrendt, W., Beckert, B., Bruns, D., Bubel, R., Gladisch, C., Grebing, S., Hähnle, R., Hentschel, M., Herda, M., Klebanov, V., Mostowski, W., Scheben, C., Schmitt, P.H., Ulbrich, M.: The key platform for verification and analysis of java programs. In: Giannakopoulou, D., Kroening, D. (eds.) VSTTE 2014. LNCS, vol. 8471, pp. 55–71. Springer, Heidelberg (2014) · Zbl 06553958 · doi:10.1007/978-3-319-12154-3_4
[2] Allen, F.E.: Control flow analysis. In: Proceedings of a Symposium on Compiler Optimization, pp. 1–19. ACM, New York (1970) · doi:10.1145/800028.808479
[3] Appel, A.W., Palsberg, J.: Modern Compiler Implementation in Java, 2nd edn. Cambridge University Press, New York (2003)
[4] Carlsson, R.: An introduction to core erlang. In: Proceedings of the PLI01 Erlang Workshop (2001)
[5] Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 3rd edn. The MIT Press, Cambridge (2009) · Zbl 1187.68679
[6] De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Semantics-based generation of verification conditions by program specialization. In: PPDP 2015, pp. 91–102. ACM (2015) · doi:10.1145/2790449.2790529
[7] de Moura, L., Bjørner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008) · Zbl 05262379 · doi:10.1007/978-3-540-78800-3_24
[8] Deters, M., Reynolds, A., King, T., Barrett, C.W., Tinelli, C.: A tour of CVC4: how it works, and how to use it. In: FMCAD 2014, p. 7. IEEE (2014) · doi:10.1109/FMCAD.2014.6987586
[9] Filliâtre, J.-C.: One logic to use them all. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 1–20. Springer, Heidelberg (2013) · Zbl 1381.68266 · doi:10.1007/978-3-642-38574-2_1
[10] 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
[11] Flanagan, C., Sabry, A., Duba, B.F., Felleisen, M.: The essence of compiling with continuations. In: PLDI 1993, pp. 237–247. ACM (1993) · doi:10.1145/155090.155113
[12] Gallagher, J.P., Kafle, B.: Analysis and transformation tools for constrained horn clause verification. CoRR, abs/1405.3883 (2014)
[13] Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: PLDI 2012, pp. 405–416. ACM (2012) · doi:10.1145/2254064.2254112
[14] Klein, G., Nipkow, T.: A machine-checked model for a java-like language, virtual machine, and compiler. ACM Trans. Program. Lang. Syst. 28(4), 619–695 (2006) · doi:10.1145/1146809.1146811
[15] Leino, K.R.M.: Developing verified programs with dafny. In: Brosgol, B., Boleng, J., Taft, S.T. (eds.) HILT, pp. 9–10. ACM (2012) · doi:10.1145/2402676.2402682
[16] Jones, S.L.P., Lester, D.R.: Implementing functional languages (Prentice Hall international series in computer science). Prentice Hall, New York (1992)
[17] Rémy, D.: Using, understanding, and unraveling the OCaml language from practice to theory and vice versa. In: Barthe, G., Dybjer, P., Pinto, L., Saraiva, J. (eds.) APPSEM 2000. LNCS, vol. 2395, p. 413. Springer, Heidelberg (2002) · Zbl 1065.68028 · doi:10.1007/3-540-45699-6_9
[18] Team, G.: Glasgow Haskell Compiler core Language. https://ghc.haskell.org/trac/ghc/wiki/Commentary/Compiler/CoreSynType
. Accessed 30 April 2015
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.