Top

International Journal on Software Tools for Technology Transfer

Published in:

20-10-2015 | TACAS 2013

Flexible SAT-based framework for incremental bounded upgrade checking

Authors: Grigory Fedyukovich, Ondrej Sery, Natasha Sharygina

Published in: International Journal on Software Tools for Technology Transfer | Issue 5/2017

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Software undergoes a myriad of minor changes along its lifecycle. Each evolved transformation of a program is expected to preserve important correctness and security properties, in particular confirmed by a software model checking tool. However, it may be extremely resource- and time-consuming to repeat entire model checking for each new version of the program. As a possible solution to this problem, we propose to conduct incremental analysis of a new program version by reusing efforts of bounded model checking of the previous program version. Our approach maintains over-approximations of the bounded program behaviors by means of function summaries derived using Craig interpolation. For each new version, these summaries are used to localize the scope of model checking. A benefit of this approach is that the cost of the upgrade checking depends on the change impact between the two versions. If the change impact is relatively small, then the incremental check can drastically outperform the model checking the new program version from scratch. We implemented the approach in scope of the SAT-based bounded model checker for C, eVolCheck. The evaluation of eVolCheck confirms that incremental changes can be verified efficiently for different classes of industrial programs.

previous article Advances in verification presented in TACAS’13

next article Synthesis of circular compositional program proofs via abduction

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now

We expect the same \(\nu \) for the old and new version. To ensure correctness, if the user increases the bound for a specific loop, the corresponding function has to be handled as if modified.

http://verify.inf.usi.ch/evolcheck.

http://www.cprover.org.

Albarghouthi, A., Gurfinkel, A., Chechik, M.: Whale: an interpolation-based algorithm for inter-procedural verification. In: VMCAI. LNCS, vol. 7148, pp. 39–55. Springer, Berlin (2012)

Backes, J.D., Person, S., Rungta, N., Tkachuk, O.: Regression verification using impact summaries. In: SPIN. LNCS, vol. 7976, pp. 99–116. Springer, Berlin (2013)

Bar-Ilan, O., Fuhrmann, O., Hoory, S., Shacham, O., Strichman, O.: Linear-time reductions of resolution proofs. In: HVC. LNCS, vol. 5394, pp. 114–128. Springer, Berlin (2008)

Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: TACAS. LNCS, vol. 1579, pp. 193–207. Springer, Berlin (1999)

Bruttomesso, R., Rollini, S., Sharygina, N., Tsitovich, A.: Flexible interpolation with local proof transformations. In: ICCAD, pp. 770–777 (2010)

Bruttomesso, R., Pek, E., Sharygina, N., Tsitovich, A.: The OpenSMT solver. In: TACAS. LNCS, vol. 6015, pp. 150–153. Springer, Berlin (2010)

Chaki, S., Clarke, E., Sharygina, N., Sinha, N.: Dynamic component substitutability analysis. In: FM. LNCS, vol. 3582, pp. 512–528. Springer, Berlin (2005)

Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: TACAS. LNCS, vol. 2988, pp. 168–176. Springer, Berlin (2004)

Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: CAV. LNCS, vol. 1855, pp. 154–169. Springer, Berlin (2000)

10.

Clarke, E.M., Kroening, D., Yorav, K.: Behavioral consistency of C and Verilog programs using bounded model checking. In: DAC, pp. 368–371. ACM, New York (2003)

11.

Cotton, S.: Two techniques for minimizing resolution proofs. In: SAT. LNCS, vol. 6175, pp. 306–312. Springer, Berlin (2010)

12.

Craig, W.: Three uses of the Herbrand–Gentzen theorem in relating model theory and proof theory. J. Symb. Logic 269–285 (1957)

13.

Cytron, R., Ferrante, J., Rosen, B., Wegman, M., Zadeck, F.: An efficient method of computing static single assignment form. In: POPL, pp. 25–35. ACM, New York (1989)

14.

Donaldson, A.F., Kroening, D., Rümmer, P.: Automatic analysis of scratch-pad memory code for heterogeneous multicore processors. In: TACAS. LNCS, vol. 6015, pp. 280–295. Springer, Berlin (2010)

15.

D’Silva, V., Kroening, D., Purandare, M., Weissenbacher, G.: Interpolant strength. In: VMCAI. LNCS, vol. 5944, pp. 129–145. Springer, Berlin (2010)

16.

Fedyukovich, G., Gurfinkel, A., Sharygina, N.: Incremental verification of compiler optimizations. In: NFM. LNCS, vol. 8430, pp. 300–306. Springer, Berlin (2014)

17.

Fedyukovich, G., D’Iddio, A.C., Hyvärinen, A.E.J., Sharygina, N.: Symbolic detection of assertion dependencies for bounded model checking. In: FASE. LNCS, vol. 9033, pp. 186–201. Springer, Berlin (2015)

18.

Fedyukovich, G., Sery, O., Sharygina, N.: eVolCheck: incremental upgrade checker for C. In: TACAS. LNCS, vol. 7795, pp. 292–307. Springer, Berlin (2013)

19.

Fedyukovich, G., Sharygina, N.: Towards completeness in bounded model checking through automatic recursion depth detection. In: SBMF. LNCS, vol. 8941, pp. 96–112. Springer, Berlin (2014)

20.

Fontaine, P., Merz, S., Paleo, B.W.: Compression of propositional resolution proofs via partial regularization. In: CADE. LNCS, vol. 6803, pp. 237–251. Springer, Berlin (2011)

21.

Godefroid, P., Lahiri, S.K., Rubio-González, C.: Statically validating must summaries for incremental compositional dynamic test generation. In: SAS. LNCS, vol. 6887. Springer, Berlin (2011)

22.

Godlin, B., Strichman, O.: Regression verification. In: DAC, pp. 466–471. ACM, New York (2009)

23.

Gurfinkel, A., Rollini, S., Sharygina, N.: Interpolation properties and SAT-based model checking. In: ATVA. LNCS, vol. 8172, pp. 255–271. Springer, Berlin (2013)

24.

Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL, pp. 232–244. ACM, New York (2004)

25.

Ivancic, F., Yang, Z., Ganai, M.K., Gupta, A., Ashar, P.: Efficient SAT-based bounded model checking for software verification. Theor. Comput. Sci. 404(3), 256–274 (2008)MathSciNetCrossRefMATH

26.

Kawaguchi, M., Lahiri, S.K., Rebelo, H.: Conditional equivalence. Tech. Rep. MSR-TR-2010-119, Microsoft Research (2010)

27.

Kroening, D., Sharygina, N., Tonetta, S., Tsitovich, A., Wintersteiger, C.M.: Loop summarization using state and transition invariants. Form. Methods Syst. Des. 42(3), 221–261 (2013)CrossRefMATH

28.

Lahiri, S.K., McMillan, K.L., Sharma, R., Hawblitzel, C.: Differential assertion checking. In: FSE, pp. 345–355. ACM, New York (2013)

29.

McMillan, K.L.: Interpolation and SAT-based model checking. In: CAV. LNCS, vol. 2725, pp. 1–13. Springer, Berlin (2003)

30.

McMillan, K.L.: Lazy annotation for program testing and verification. In: CAV. LNCS, vol. 6174, pp. 104–118. Springer, Berlin (2010)

31.

Merz, F., Falke, S., Sinz, C.: LLBMC: bounded model checking of C and C++ programs using a compiler IR. In: VSTTE. LNCS, vol. 7152, pp. 146–161. Springer, Berlin (2012)

32.

Person, S., Dwyer, M.B., Elbaum, S.G., Pasareanu, C.S.: Differential symbolic execution. In: FSE, pp. 226–237. ACM, New York (2008)

33.

Pudlák, P.: Lower bounds for resolution and cutting plane proofs and monotone computations. J. Symb. Log. 62(3), 981–998 (1997)MathSciNetCrossRefMATH

34.

Rollini, S.F., Alt, L., Fedyukovich, G., Hyvärinen, A.E.J., Sharygina, N.: PeRIPLO: a framework for producing effective interpolants in SAT-based software verification. In: LPAR. LNCS, vol. 8312, pp. 683–693. Springer, Berlin (2013)

35.

Rollini, S.F., Bruttomesso, R., Sharygina, N.: An efficient and flexible approach to resolution proof reduction. In: HVC. LNCS, vol. 6504, pp. 182–196. Springer, Berlin (2010)

36.

Rollini, S.F., Sery, O., Sharygina, N.: Leveraging interpolant strength in model checking. In: CAV. LNCS, vol. 7358, pp. 193–209. Springer, Berlin (2012)

37.

Sery, O., Fedyukovich, G., Sharygina, N.: FunFrog: bounded model checking with interpolation-based function summarization. In: ATVA. LNCS, vol. 7561, pp. 203–207. Springer, Berlin (2012)

38.

Sery, O., Fedyukovich, G., Sharygina, N.: Incremental upgrade checking by means of interpolation-based function summaries. In: FMCAD, pp. 114–121. IEEE (2012)

39.

Sery, O., Fedyukovich, G., Sharygina, N.: Interpolation-based function summaries in bounded model checking. In: HVC. LNCS, vol. 7261, pp. 160–175. Springer, Berlin (2012)

40.

Yang, G., Khurshid, S., Person, S., Rungta, N.: Property differencing for incremental checking. In: ICSE, pp. 1059–1070. ACM, New York (2014)

Title: Flexible SAT-based framework for incremental bounded upgrade checking
Authors: Grigory Fedyukovich
Ondrej Sery
Natasha Sharygina
Publication date: 20-10-2015
Publisher: Springer Berlin Heidelberg
Published in: International Journal on Software Tools for Technology Transfer / Issue 5/2017
Print ISSN: 1433-2779
Electronic ISSN: 1433-2787
DOI: https://doi.org/10.1007/s10009-015-0405-y

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Other articles of this Issue 5/2017

Synthesis of circular compositional program proofs via abduction

Advances in verification presented in TACAS’13

An integrated specification and verification technique for highly concurrent data structures for highly concurrent data structures

Efficient family-based model checking via variability abstractions

metaSMT: focus on your application and not on solver integration

A general model checking framework for various memory consistency models

Premium Partner