Advertisement

LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes

  • Alejandro Sánchez
  • César Sánchez
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8559)

Abstract

This tool paper describes Leap, a tool for the verification of concurrent datatypes and parametrized systems composed by an unbounded number of threads that manipulate infinite data.

Leap receives as input a concurrent program description and a specification and automatically generates a finite set of verification conditions which are then discharged to specialized decision procedures. The validity of all discharged verification conditions implies that the program executed by any number of threads satisfies the specification. Currently, Leap includes not only decision procedures for integers and Booleans, but it also implements specific theories for heap memory layouts such as linked-lists and skiplists.

Keywords

Decision Procedure Concurrent Program Liveness Property Proof Rule Separation Logic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    Abdulla, P.A., Bouajjani, A., Jonsson, B., Nilsson, M.: Handling global conditions in parametrized system verification. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 134–145. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  2. 2.
    Abdulla, P.A., Delzanno, G., Rezine, A.: Approximated parameterized verif. of infinite-state processes with global conditions. FMSD 34(2), 126–156 (2009)MATHGoogle Scholar
  3. 3.
    Apt, K.R., Kozen, D.C.: Limits for automatic verification of finite-state concurrent systems. Information Processing Letters 22(6), 307–309 (1986)CrossRefMathSciNetGoogle Scholar
  4. 4.
    Berdine, J., Calcagno, C., O’Hearn, P.W.: Smallfoot: Modular automatic assertion checking with separation logic. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 115–137. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  5. 5.
    Bradley, A.R., Manna, Z., Sipma, H.B.: What’s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 427–442. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  6. 6.
    Browne, I.A., Manna, Z., Sipma, H.B.: Generalized verification diagrams. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol. 1026, pp. 484–498. Springer, Heidelberg (1995)CrossRefGoogle Scholar
  7. 7.
    Chaudhuri, K., Doligez, D., Lamport, L., Merz, S.: The TLA +  proof system: Building a heterogeneous verification platform. In: Cavalcanti, A., Deharbe, D., Gaudel, M.-C., Woodcock, J. (eds.) ICTAC 2010. LNCS, vol. 6255, p. 44. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  8. 8.
    Clarke, E.M., Grumberg, O.: Avoiding the state explosion problem in temporal logic model checking. In: Proc. of PODC 1987, pp. 294–303. ACM (1987)Google Scholar
  9. 9.
    Clarke, E.M., Grumberg, O., Browne, M.C.: Reasoning about networks with many identical finite-state procs. In: Proc. of PODC 1986, pp. 240–248. ACM (1986)Google Scholar
  10. 10.
    Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: A practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23–42. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  11. 11.
    Condit, J., Hackett, B., Lahiri, S.K., Qadeer, S.: Unifying type checking and property checking for low-level code. In: Proc. of POPL 2009, pp. 302–314. ACM Press (2009)Google Scholar
  12. 12.
    Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C – a software analysis perspective. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 233–247. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  13. 13.
    de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  14. 14.
    Emerson, E.A., Kahlon, V.: Reducing model checking of the many to the few. In: McAllester, D. (ed.) CADE-17. LNCS (LNAI), vol. 1831, pp. 236–254. Springer, Heidelberg (2000)Google Scholar
  15. 15.
    Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast decision procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 175–188. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  16. 16.
    Herlihy, M., Shavit, N.: The Art of Multiprocessor Programming. Morgan- Kaufmann (2008)Google Scholar
  17. 17.
    Kuncak, V., Rinard, M.C.: An overview of the Jahob analysis system: Project goals and current status. In: Proc. of IPDPS 2006. IEEE Computer Society Press (2006)Google Scholar
  18. 18.
    Leino, K.R.M.: Verifying concurrent programs with Chalice. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, p. 2. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  19. 19.
    Manna, Z., Anuchitanukul, A., Bjørner, N., Browne, A., Chang, E., Colón, M., de Alfaro, L., Devarajan, H., Sipma, H., Uribe, T.: STeP: The stanford temporal prover. Technical Report STAN-CS-TR-94-1518, Computer Science Department, Stanford University (July 1994)Google Scholar
  20. 20.
    Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems. Springer (1995)Google Scholar
  21. 21.
    Bozzano, M., Delzanno, G.: Beyond parameterized verification. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 221–235. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  22. 22.
    Podelsky, A., Rybalchenko, A.: Transition invariants. In: Proc. of LICS 2004, pp. 32–41. IEEE Computer Society Press (2004)Google Scholar
  23. 23.
    Sánchez, A., Sánchez, C.: Decision procedure for the temporal verification of concurrent lists. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol. 6447, pp. 74–89. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  24. 24.
    Sánchez, A., Sánchez, C.: A theory of skiplists with applications to the verification of concurrent datatypes. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 343–358. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  25. 25.
    Sánchez, A., Sánchez, C.: Parametrized invariance for infinite state processes. CoRR, abs/1312.4043 (2013)Google Scholar
  26. 26.
    Sanchez, A., Sankaranarayanan, S., Sánchez, C., Chang, B.-Y.E.: Invariant generation for parametrized systems using self-reflection. In: Miné, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 146–163. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  27. 27.
    Sánchez, C., Sánchez, A.: A decidable theory of skiplists of unbounded size and arbitrary height. CoRR, abs/1301.4372 (2013)Google Scholar
  28. 28.
    Smans, J., Jacobs, B., Piessens, F.: Vericool: An automatic verifier for a concurrent object-oriented language. In: Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol. 5051, pp. 220–239. Springer, Heidelberg (2008)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Alejandro Sánchez
    • 1
  • César Sánchez
    • 1
    • 2
  1. 1.IMDEA Software InstituteMadridSpain
  2. 2.Institute for Information Security, CSICSpain

Personalised recommendations