nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

Incremental Verification Using Trace Abstraction

verfasst von : Bat-Chen Rothenberg, Daniel Dietsch, Matthias Heizmann

Erschienen in: Static Analysis

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Invertible Linear Transforms of Numerical Abstract Domains

Nächstes Kapitel Volume-Based Merge Heuristics for Disjunctive Numeric Domains

https://ultimate.informatik.uni-freiburg.de.

https://github.com/ultimate-pa.

https://www.sosy-lab.org/research/cpa-reuse/regression-benchmarks.

https://sv-comp.sosy-lab.org/2018/.

https://ultimate.informatik.uni-freiburg.de/smtinterpol, version 2.1-441-gf99e49f.

https://github.com/Z3Prover/z3, version master 450f3c9b.

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)

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_7CrossRef

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_15CrossRef

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)

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)

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)

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_9CrossRefMATH

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)

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)

10.

Chockler, H., Kroening, D., Mariani, L., Sharygina, N.: Validation of Evolving Software. Springer, Heidelberg (2015)CrossRef

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)

12.

Fedyukovich, G., Gurfinkel, A., Sharygina, N.: Incremental verification of compiler optimizations. In: NASA Formal Methods, pp. 300–306 (2014)

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)

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_30CrossRef

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_17CrossRef

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_7CrossRef

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_2CrossRef

18.

Heizmann, M. et al.: Automizer and the search for perfect interpolants. In: TACAS 2018 (2018, to appear)

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)

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_8CrossRef

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)

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)

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)

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_54CrossRef

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_39CrossRef

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_20CrossRef

27.

Venkatesh, M.B.: A case study in non-functional regression verification (2016)

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)

Titel: Incremental Verification Using Trace Abstraction
verfasst von: Bat-Chen Rothenberg
Daniel Dietsch
Matthias Heizmann
Verlag: Springer International Publishing
Buch: Static Analysis
Print ISBN: 978-3-319-99724-7

Electronic ISBN: 978-3-319-99725-4

Copyright-Jahr: 2018
DOI: https://doi.org/10.1007/978-3-319-99725-4_22

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"