nach oben

Software and Systems Modeling

Erschienen in:

01.02.2015 | Special Section Paper

TacoFlow: optimizing SAT program verification using dataflow analysis

verfasst von: Bruno Cuervo Parrino, Juan Pablo Galeotti, Diego Garbervetsky, Marcelo F. Frias

Erschienen in: Software and Systems Modeling | Ausgabe 1/2015

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

In previous work, we presented TACO, a tool for efficient bounded verification. TACO translates programs annotated with contracts to a SAT problem which is then solved resorting to off-the-shelf SAT-solvers. TACO may deem propositional variables used in the description of a program initial states as being unnecessary. Since the worst-case complexity of SAT (a known NP problem) depends on the number of variables, most times this allows us to obtain significant speed ups. In this article, we present TacoFlow, an improvement over TACO that uses dataflow analysis in order to also discard propositional variables that describe intermediate program states. We present an extensive empirical evaluation that considers the effect of removing those variables at different levels of abstraction, and a discussion on the benefits of the proposed approach.

Vorheriger Artikel Verification of B trees by integration of shape analysis and interactive theorem proving

Nächster Artikel Model checking LTL properties over ANSI-C programs with bounded traces

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 "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

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

For the sake of simplicity and presentation, we avoid showing the case for \(entry\) in the definitions of \(f\) and \(\hat{f}\).

In the Single Static Assignment (SSA) form, each variable is defined exactly once.

TacoFlow and the benchmark are available at http://www.dc.uba.ar/tacoflow.

Alpern, B., Wegman, M.N., Zadeck, F.K.: Detecting equality of variables in programs. In Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 1–11. ACM (1988)

Belt, J., Robby., Deng, X.: Sireum/Topi LDP: a lightweight semi-decision procedure for optimizing symbolic execution-based analyses. In: Proceedings of the 7th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on The foundations of software engineering, pp. 355–364. ACM (2009)

Biere, A.: Pre,icoSAT@SC’09. Solver description for sat competition 2009. In: In SAT 2009 Competitive Event Booklet (2009)

Biere, A., Biere, A., Heule, M., van Maaren, H., Walsh, T.: Handbook of Satisfiability: Volume 185 Frontiers in Artificial Intelligence and Applications. IOS Press, Amsterdam (2009)

Blanc, N., Kroening, D., Sharygina, N.: Scoot: A tool for the analysis of SystemC models. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008), LNCS, vol. 4963, pp. 467–470 (2008)

Boyapati, C., Khurshid, S., Marinov, D.: Korat: automated testing based on java predicates. In: Proceedings of the 2002 ACM SIGSOFT International Symposium on Software Testing and Analysis, pp. 123–133. ACM (2002)

Chalin, P., Kiniry, J.R., Leavens, G.T., Poll, E.: Beyond assertions: advanced specification and verification with jml and esc/java2. In: Proceedings of the 4th International Conference on Formal Methods for Components and Objects, pp. 342–363. Springer (2006)

Clarke, E., Kroening, D., Lerda, F.: A tool for checking ansi-c programs. In: In Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004), LNCS, vol. 2988, pp. 168–176. Springer (2004)

Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: SATABS: SAT-based predicate abstraction for ANSI-C. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005), Lecture Notes in Computer Science, vol. 3440, pp. 570–574. Springer (2005)

10.

Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 269–282. ACM (1979)

11.

Cousot, P., Cousot, R.: Abstract interpretation and application to logic programs. J. Log. Program. 13(2–3), 103–179 (1992)CrossRefMATHMathSciNet

12.

Crawford, J., Ginsberg, M., Luks, E., Roy, A.: Symmetry-breaking predicates for search problems. In: Principles of Knowledge Representation and Reasoning, pp. 148–159 (1996)

13.

Dennis, G., Yessenov, K., Jackson, D.: Bounded verification of voting software. In: Proceedings of the 2nd International Conference on Verified Software: Theories, Tools, Experiments, pp. 130–145. Springer (2008)

14.

Dolby, J., Vaziri, M., Tip, F.: Finding bugs efficiently with a sat solver. In: Proceedings of the 6th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on The Foundations of Software Engineering, ESEC-FSE ’07, pp. 95–204, New York, NY, USA, ACM (2007)

15.

Eén, N., Sörensson, N.: An extensible sat-solver. In: Giunchiglia, E., Tacchella, A., (eds.), SAT, Lecture Notes in Computer Science, vol. 2919, pp. 502–518. Springer (2003)

16.

Frias, M., Galeotti, J.P., López Pombo, C., Aguirre, N. Dynalloy: upgrading alloy with actions. In: Proceedings of the 27th International Conference on Software Engineering, pp. 442–451. ACM (2005)

17.

Galeotti, J.P.: Software Verification Using Alloy. PhD thesis, University of Buenos Aires (2010)

18.

Galeotti, J.P., Rosner, N., López Pombo, C., Frias, M.: Analysis of invariants for efficient bounded verification. In: Proceedings of the 19th International Symposium on Software Testing and Analysis, pp. 25–36. ACM (2010)

19.

Harel, D., Kozen, D., Jerzy, T.: Dynamic Logic. The MIT Press, Cambridge (2000)MATH

20.

Ivancic, F., Yang, Z., Ganai, M.K., Gupta, A., Shlyakhter, I., Ashar, P.: F-soft: Software verification platform. In CAV’05, pp. 301–306 (2005)

21.

Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol. 11(2), 256–290 (2002)CrossRef

22.

Jackson, D.: Software Abstractions: Logic, Language, and Analysis (Revised Edition). The MIT Press, Cambridge (2012)

23.

Jackson, D., Vaziri, M.: Finding bugs with a constraint solver. In: Proceedings of the 2000 ACM SIGSOFT International Symposium on Software Testing and Analysis, pp. 14–25. ACM (2000)

24.

Kildall, G.A.: A unified approach to global program optimization. In: Proceedings of the 1st Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 194–206. ACM (1973)

25.

Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, New York (1999)CrossRefMATH

26.

Nielson, Flemming: A denotational framework for data flow analysis. Acta Inform. 18, 265–287 (1982)CrossRefMATHMathSciNet

27.

Post, H., Sinz, C., Küchlin, W.: Towards automatic software model checking of thousands of linux modules—a case study with avinux. Softw. Test. Verif. Reliab. 19(2), 155–172 (2009)CrossRef

28.

Shao, D., Gopinath, D., Khurshid, S., Perry, D.E.: Optimizing incremental scope-bounded checking with data-flow analysis. In: Proceedings of the 2010 IEEE 21st International Symposium on Software Reliability Engineering, pp. 408–417. IEEE Computer Society (2010)

29.

Sharma, R., Gligoric, M., Arcuri, A., Fraser, G., Marinov, D.: Testing container classes: random or systematic? In: Proceedings of the 14th International Conference on Fundamental Approaches to Software Engineering: Part of the Joint European Conferences on Theory and Practice of Software, FASE’11/ETAPS’11, pp. 262–277. Springer (2011)

30.

Siddiqui, J.H., Khurshid, S.: An empirical study of structural constraint solving techniques. In: Proceedings of the 11th International Conference on Formal Engineering Methods: Formal Methods and Software Engineering, pp. 88–106. Springer (2009)

31.

Taghdiri, M., Seater, R., Jackson, D.: Lightweight extraction of syntactic specifications. In: Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 276–286. ACM (2006)

32.

Torlak, E., Jackson, E.: Kodkod: a relational model finder. In: Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 632–647. Springer (2007)

33.

Visser, W., Pǎsǎreanu, C.S., Pelánek, R.: Test input generation for java containers using state matching. In: Proceedings of the 2006 International Symposium on Software Testing and Analysis, pp. 37–48. ACM (2006)

34.

Xie, Y., Aiken, A.: Saturn: a scalable framework for error detection using boolean satisfiability. ACM Trans. Program. Lang. Syst. 29, 16-es (2007)

35.

Yessenov, K.: A light-weight specification language for bounded program verification. Master’s thesis, MIT (2009)

Titel: TacoFlow: optimizing SAT program verification using dataflow analysis
verfasst von: Bruno Cuervo Parrino
Juan Pablo Galeotti
Diego Garbervetsky
Marcelo F. Frias
Publikationsdatum: 01.02.2015
Verlag: Springer Berlin Heidelberg
Erschienen in: Software and Systems Modeling / Ausgabe 1/2015
Print ISSN: 1619-1366
Elektronische ISSN: 1619-1374
DOI: https://doi.org/10.1007/s10270-014-0401-9

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 "Wirtschaft"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 1/2015

SEFM: software engineering and formal methods

Runtime verification of component-based systems in the BIP framework with formally-proved sound and complete instrumentation

The 2014 “State of the Journal” report

Improving the SAT modulo ODE approach to hybrid systems analysis by combining different enclosure methods

Environment modeling and simulation for automated testing of soft real-time embedded software

A fine-grained analysis of the support provided by UML class diagrams and ER diagrams during data model maintenance

Premium Partner