Advertisement

Incremental Verification Using Trace Abstraction

  • Bat-Chen RothenbergEmail author
  • Daniel Dietsch
  • Matthias Heizmann
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11002)

Abstract

Despite the increasing effectiveness of model checking tools, automatically re-verifying a program whenever a new revision of it is created is often not feasible using existing tools. Incremental verification aims at facilitating this re-verification, by reusing partial results. In this paper, we propose a novel approach for incremental verification that is based on trace abstraction. Trace abstraction is an automata-based verification technique in which the program is proved correct using a sequence of automata. We present two algorithms that reuse this sequence across different revisions, one eagerly and one lazily. We demonstrate their effectiveness in an extensive experimental evaluation on a previously established benchmark set for incremental verification based on different revisions of device drivers from the Linux kernel. Our algorithm is able to achieve significant speedups on this set, compared to both stand-alone verification and previous approaches.

References

  1. 1.
    Adler, J., Berryhill, R., Veneris, A.: Revision debug with non-linear version history in regression verification. In: IEEE International Verification and Security Workshop (IVSW), pp. 1–6. IEEE (2016)Google Scholar
  2. 2.
    Backes, J., Person, S., Rungta, N., Tkachuk, O.: Regression verification using impact summaries. In: Bartocci, E., Ramakrishnan, C.R. (eds.) SPIN 2013. LNCS, vol. 7976, pp. 99–116. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-39176-7_7CrossRefGoogle Scholar
  3. 3.
    Beckert, B., Ulbrich, M., Vogel-Heuser, B., Weigl, A.: Regression verification for programmable logic controller software. In: Butler, M., Conchon, S., Zaïdi, F. (eds.) ICFEM 2015. LNCS, vol. 9407, pp. 234–251. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-25423-4_15CrossRefGoogle Scholar
  4. 4.
    Beyer, D., Löwe, S., Novikov, E., Stahlbauer, A., Wendler, P.: Precision reuse for efficient regression verification. In: Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering, pp. 389–399 (2013)Google Scholar
  5. 5.
    Bohme, M., Oliveira, B.C.D.S., Roychoudhury, A., Böhme, M.: Partition-based regression verification. In: Proceedings of the 2013 International Conference on Software Engineering, pp. 302–311. IEEE Press (2013)Google Scholar
  6. 6.
    Brandin, B., Malik, R., Dietrich, P.: Incremental system verification and synthesis of minimally restrictive behaviours. In: Proceedings of the 2000 American Control Conference, vol. 6, pp. 4056–4061. IEEE (2000)Google Scholar
  7. 7.
    Chaki, S., Gurfinkel, A., Strichman, O.: Regression verification for multi-threaded programs. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 119–135. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-27940-9_9CrossRefzbMATHGoogle Scholar
  8. 8.
    Chang, K.-H., Papa, D.A., Markov, I.L., Bertacco, V.: InVerS: an incremental verification system with circuit similarity metrics and error visualization. In: 2007 8th International Symposium on Quality Electronic Design, ISQED 2007, pp. 487–494. IEEE (2007)Google Scholar
  9. 9.
    Chockler, H., Ivrii, A., Matsliah, A., Moran, S., Nevo, Z.: Incremental formal verification of hardware. In: Proceedings of the International Conference on Formal Methods in Computer-Aided Design, pp. 135–143. FMCAD Inc. (2011)Google Scholar
  10. 10.
    Chockler, H., Kroening, D., Mariani, L., Sharygina, N.: Validation of Evolving Software. Springer, Heidelberg (2015)CrossRefGoogle Scholar
  11. 11.
    Dietsch, D., Heizmann, M., Musa, B., Nutz, A., Podelski, A.: Craig vs. Newton in software model checking. In: ESEC/FSE 2017, pp. 487–497 (2017)Google Scholar
  12. 12.
    Fedyukovich, G., Gurfinkel, A., Sharygina, N.: Incremental verification of compiler optimizations. In: NASA Formal Methods, pp. 300–306 (2014)Google Scholar
  13. 13.
    Felsing, D., Grebing, S., Klebanov, V., Rümmer, P., Ulbrich, M.: Automating regression verification. In: 29th IEEE/ACM International Conference on Automated Software Engineering, ASE 2014, pp. 349–360 (2014)Google Scholar
  14. 14.
    Forejt, V., Kwiatkowska, M., Parker, D., Qu, H., Ujma, M.: Incremental runtime verification of probabilistic systems. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 314–319. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-35632-2_30CrossRefGoogle Scholar
  15. 15.
    He, F., Mao, S., Wang, B.-Y.: Learning-based assume-guarantee regression verification. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 310–328. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-41528-4_17CrossRefGoogle Scholar
  16. 16.
    Heizmann, M., Hoenicke, J., Podelski, A.: Refinement of trace abstraction. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol. 5673, pp. 69–85. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-03237-0_7CrossRefGoogle Scholar
  17. 17.
    Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 36–52. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-39799-8_2CrossRefGoogle Scholar
  18. 18.
    Heizmann, M. et al.: Automizer and the search for perfect interpolants. In: TACAS 2018 (2018, to appear)Google Scholar
  19. 19.
    Johnson, K., Calinescu, R., Kikuchi, S.: An incremental verification framework for component-based software systems. In: Proceedings of the 16th International ACM SIGSOFT Symposium on Component-Based Software Engineering, pp. 33–42. ACM (2013)Google Scholar
  20. 20.
    Lakhnech, Y., Bensalem, S., Berezin, S., Owre, S.: Incremental verification by abstraction. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 98–112. Springer, Heidelberg (2001).  https://doi.org/10.1007/3-540-45319-9_8CrossRefGoogle Scholar
  21. 21.
    Maksimovic, D., Veneris, A., Poulos, Z.: Clustering-based revision debug in regression verification. In: Proceedings of the 33rd IEEE International Conference on Computer Design, ICCD 2015, pp. 32–37 (2015)Google Scholar
  22. 22.
    Meseguer, P.: Incremental verification of rule-based expert systems. In: Proceedings of the 10th European Conference on Artificial Intelligence, pp. 840–844. Wiley (1992)Google Scholar
  23. 23.
    Sery, O., Fedyukovich, G., Sharygina, N.: Incremental upgrade checking by means of interpolation-based function summaries. In: Formal Methods in Computer-Aided Design, FMCAD 2012, Cambridge, UK, 22–25 October 2012, pp. 114–121 (2012)Google Scholar
  24. 24.
    Strichman, O., Godlin, B.: Regression verification - a practical way to verify programs. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol. 4171, pp. 496–501. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-69149-5_54CrossRefGoogle Scholar
  25. 25.
    Strichman, O., Veitsman, M.: Regression verification for unbalanced recursive functions. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 645–658. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-48989-6_39CrossRefGoogle Scholar
  26. 26.
    Trostanetski, A., Grumberg, O., Kroening, D.: Modular demand-driven analysis of semantic difference for program versions. In: Ranzato, F. (ed.) SAS 2017. LNCS, vol. 10422, pp. 405–427. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-66706-5_20CrossRefGoogle Scholar
  27. 27.
    Venkatesh, M.B.: A case study in non-functional regression verification (2016)Google Scholar
  28. 28.
    Visser, W., Geldenhuys, J., Dwyer, M.B.: Green: reducing, reusing and recycling constraints in program analysis. In: Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering, pp. 58:1–58:11 (2012)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Bat-Chen Rothenberg
    • 1
    Email author
  • Daniel Dietsch
    • 2
  • Matthias Heizmann
    • 2
  1. 1.Technion - Israel Institute of TechnologyHaifaIsrael
  2. 2.University of FreiburgFreiburgGermany

Personalised recommendations