×

Verification by parallelization of parametric code. (English) Zbl 1122.68037

Aguzzoli, Stefano (ed.) et al., Algebraic and proof-theoretic aspects of non-classical logics. Papers in honor of Daniele Mundici on the occasion of his 60th birthday. Berlin: Springer (ISBN 978-3-540-75938-6/pbk). Lecture Notes in Computer Science 4460. Lecture Notes in Artificial Intelligence, 138-159 (2007).
Summary: Loops and other unbound control structures constitute a major bottleneck in formal software verification, because correctness proofs over such control structures generally require user interaction: typically, induction hypotheses or invariants must be found or modified by hand. Such interaction involves expert knowledge of the underlying calculus and proof engine. We show that one can replace interactive proof techniques, such as induction, with automated first-order reasoning in order to deal with parallelizable loops. A loop can be parallelized, whenever the execution of a generic iteration of its body depends only on the step parameter and not on other iterations. We use a symbolic dependence analysis that ensures parallelizability. This guarantees soundness of a proof rule that transforms a loop into a universally quantified update of the state change information effected by the loop body. This rule makes it possible to employ automatic first-order reasoning techniques to deal with loops. The method has been implemented in the KeY verification tool. We evaluated its applicability with representative case studies from the Java Card domain.
For the entire collection see [Zbl 1121.03003].

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Software:

Spec#; ESC/Java; NQTHM
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Banerjee, U., Chen, S.-C., Kuck, D.J., Towle, R.A.: Time and parallel processor bounds for Fortran-like loops. IEEE Trans. Computers 28(9), 660–670 (1979) · Zbl 0419.68020 · doi:10.1109/TC.1979.1675434
[2] Barnett, M., Leino, K.R.M., 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
[3] Beckert, B.: A dynamic logic for the formal verification of Java Card programs. In: Attali, I., Jensen, T. (eds.) JavaCard 2000. LNCS, vol. 2041, pp. 6–24. Springer, Heidelberg (2001) · Zbl 0980.68525 · doi:10.1007/3-540-45165-X_2
[4] Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007)
[5] Beckert, B., Schlager, S.: Software verification with integrated data type refinement for integer arithmetic. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol. 2999, pp. 207–226. Springer, Heidelberg (2004) · Zbl 1196.68126 · doi:10.1007/978-3-540-24756-2_12
[6] Beckert, B., Schlager, S., Schmitt, P.H.: An improved rule for while loops in deductive program verification. In: Lau, K.-K., Banach, R. (eds.) ICFEM 2005. LNCS, vol. 3785, Springer, Heidelberg (2005) · doi:10.1007/11576280_22
[7] Boyer, R.S., Moore, J S.: A Computational Logic Handbook. Academic Press, London (1988) · Zbl 0655.68117
[8] Breunesse, C.-B.: On JML: Topics in Tool-assisted Verification of Java Programs. PhD thesis, Radboud University of Nijmegen (2006)
[9] Bundy, A., Basin, D., Hutter, D., Ireland, A.: Rippling: Meta-Level Guidance for Mathematical Reasoning, June 2005. Cambridge Tracts in Theoretical Computer Science, vol. 56. Cambridge University Press, Cambridge (2005) · Zbl 1095.68108 · doi:10.1017/CBO9780511543326
[10] Burdy, L., Requet, A., Lanet, J.-L.: Java applet correctness: a developer-oriented approach. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 422–439. Springer, Heidelberg (2003) · doi:10.1007/978-3-540-45236-2_24
[11] Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: Schwartzbach, M.I., Ball, T. (eds.) Proc. ACM SIGPLAN Conf. on Programming Language Design and Implementation, Ottawa, Canada, pp. 415–426. ACM Press, New York (2006)
[12] Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Proc. ACM SIGPLAN 2002 Conf. on Programming Language Design and Implementation, Berlin, pp. 234–245. ACM Press, New York (2002) · doi:10.1145/512529.512558
[13] Gedell, T., Hähnle, R.: Automating verification of loops by parallelization. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 332–346. Springer, Heidelberg (2006) · Zbl 1165.68405 · doi:10.1007/11916277_23
[14] Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000) · Zbl 0976.68108
[15] Holzmann, G.J.: Software analysis and model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 1–16. Springer, Heidelberg (2002) · Zbl 1010.68789 · doi:10.1007/3-540-45657-0_1
[16] Jacobs, B., Marché, C., Rauch, N.: Formal verification of a commercial smart card applet with multiple tools. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116, pp. 241–257. Springer, Heidelberg (2004) · Zbl 1108.68391 · doi:10.1007/978-3-540-27815-3_21
[17] Leino, K.R.M., Logozzo, F.: Loop invariants on demand. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 119–134. Springer, Heidelberg (2005) · Zbl 1159.68374 · doi:10.1007/11575467_9
[18] Marché, C., Paulin-Mohring, C.: Reasoning about Java programs with aliasing and frame conditions. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 179–194. Springer, Heidelberg (2005) · Zbl 1152.68524 · doi:10.1007/11541868_12
[19] Mostowski, W.: Formalisation and verification of Java Card security properties in dynamic logic. In: Cerioli, M. (ed.) FASE 2005. LNCS, vol. 3442, pp. 357–371. Springer, Heidelberg (2005) · Zbl 1119.68351 · doi:10.1007/978-3-540-31984-9_27
[20] Olsson, O., Wallenburg, A.: Customised induction rules for proving correctness of imperative programs. In: Beckert, B., Aichernig, B. (eds.) Proc. Software Engineering and Formal Methods (SEFM), Koblenz, Germany, pp. 180–189. IEEE Press, Los Alamitos (2005)
[21] Platzer, A.: Using a program verification calculus for constructing specifications from implementations. Master’s thesis, Univ. Karlsruhe, Dept. of Computer Science (2004)
[22] Poetzsch-Heffter, A., Müller, P.: A Programming Logic for Sequential Java. In: Swierstra, S.D. (ed.) ESOP 1999 and ETAPS 1999. LNCS, vol. 1576, pp. 162–176. Springer, Heidelberg (1999) · doi:10.1007/3-540-49099-X_11
[23] Rodríguez-Carbonell, E., Kapur, D.: Program verification using automatic generation of invariants. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol. 3407, pp. 325–340. Springer, Heidelberg (2005) · Zbl 1108.68520 · doi:10.1007/978-3-540-31862-0_24
[24] Rümmer, P.: Sequential, parallel, and quantified updates of first-order structures. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 422–436. Springer, Heidelberg (2006) · Zbl 1165.68376 · doi:10.1007/11916277_29
[25] Schroeder, M.: Using a symbolic dependence analysis for verification of programs containing loops. Master’s thesis, Department of Computer Science, University of Karlsruhe (2007)
[26] Stenzel, K.: Verification of Java Card Programs. PhD thesis, Fakultät für angewandte Informatik, University of Augsburg (2005)
[27] Sun Microsystems, Inc.: Santa Clara, California, USA. JAVA CARD 2.2.1 Application Programming Interface (October 2003)
[28] Wolfe, M.J.: Optimizing Supercompilers for Supercomputers. MIT Press, Cambridge (1989) · Zbl 0699.68007
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.