Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Partial Evaluation of Order-Sorted Equational Programs Modulo Axioms Kapitel lesen Erstes Kapitel lesen

2017 | OriginalPaper | Buchkapitel

Scaling Bounded Model Checking by Transforming Programs with Arrays

verfasst von : Anushri Jana, Uday P. Khedker, Advaita Datar, R. Venkatesh, Niyas C.

Erschienen in: Logic-Based Program Synthesis and Transformation

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

Bounded Model Checking is one the most successful techniques for finding bugs in program. However, model checkers are resource hungry and are often unable to verify programs with loops iterating over large arrays. We present a transformation that enables bounded model checkers to verify a certain class of array properties. Our technique transforms an array-manipulating (Ansi-C) program to an array-free and loop-free (Ansi-C) program thereby reducing the resource requirements of a model checker significantly. Model checking of the transformed program using an off-the-shelf bounded model checker simulates the loop iterations efficiently. Thus, our transformed program is a sound abstraction of the original program and is also precise in a large number of cases—we formally characterize the class of programs for which it is guaranteed to be precise. We demonstrate the applicability and usefulness of our technique on both industry code as well as academic benchmarks.

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 A Reversible Semantics for Erlang
Nächstes Kapitel Intuitionistic Logic Programming for SQL
Fußnoten
2
Results of analysis may be over-approximated.
 
3
Programs in ArrayMemSafety access arrays without using index and cannot be transformed.
 
6
PRISM implements [22] for slicing.
 
Literatur
1.
2.
3.
Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: An extension of lazy abstraction with interpolation for programs with arrays. In: Formal Methods in System Design (2014)
4.
Alberti, F., Ghilardi, S., Sharygina, N.: Booster: an acceleration-based verification framework for array programs. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 18–23. Springer, Cham (2014). doi:10.​1007/​978-3-319-11936-6_​2
5.
Alberti, F., Monniaux, D.: Polyhedra to the rescue of array interpolants. In: Annual ACM Symposium on Applied Computing (2015)
6.
Ball, T., Rajamani, S.K.: The slam project: debugging system software via static analysis. In: ACM SIGPLAN Notices, vol. 37 (2002)
7.
Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Invariant synthesis for combined theories. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 378–394. Springer, Heidelberg (2007). doi:10.​1007/​978-3-540-69738-1_​27 CrossRef
8.
Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In: Mogensen, T.Æ., Schmidt, D.A., Sudborough, I.H. (eds.) The Essence of Computation. LNCS, vol. 2566, pp. 85–108. Springer, Heidelberg (2002). doi:10.​1007/​3-540-36377-7_​5 CrossRef
9.
10.
Chimdyalwar, B., Kumar, S.: Effective false positive filtering for evolving software. In: ISEC (2011)
11.
Copty, F., Fix, L., Fraer, R., Giunchiglia, E., Kamhi, G., Tacchella, A., Vardi, M.Y.: Benefits of bounded model checking at an industrial setting. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 436–453. Springer, Heidelberg (2001). doi:10.​1007/​3-540-44585-4_​43 CrossRef
12.
Cornish, J.R.M., Gange, G., Navas, J.A., Schachte, P., Søndergaard, H., Stuckey, P.J.: Analyzing array manipulating programs by program transformation. In: Proietti, M., Seki, H. (eds.) LOPSTR 2014. LNCS, vol. 8981, pp. 3–20. Springer, Cham (2015). doi:10.​1007/​978-3-319-17822-6_​1
13.
Cousot, P., Cousot, R., Logozzo, F.: A parametric segmentation functor for fully automatic and scalable array content analysis. In: ACM SIGPLAN Notices, vol. 46 (2011)
14.
Darke, P., Chimdyalwar, B., Venkatesh, R., Shrotri, U., Metta, R.: Over-approximating loops to prove properties using bounded model checking. In: DATE (2015)
15.
De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: A rule-based verification strategy for array manipulating programs. Fundamenta Informaticae 140, 329–355 (2015)MathSciNetCrossRefMATH
16.
17.
Fähndrich, M., Logozzo, F.: Static contract checking with abstract interpretation. In: Beckert, B., Marché, C. (eds.) FoVeOOS 2010. LNCS, vol. 6528, pp. 10–30. Springer, Heidelberg (2011). doi:10.​1007/​978-3-642-18070-5_​2 CrossRef
18.
Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. ACM SIGPLAN Not. 37, 191–202 (2002)CrossRefMATH
19.
Gopan, D., Reps, T., Sagiv, M.: A framework for numeric analysis of array operations. ACM SIGPLAN Not. 40(1), 338–350 (2005)CrossRefMATH
20.
Gulwani, S., McCloskey, B., Tiwari, A.: Lifting abstract interpreters to quantified logical domains. In: POPL (2008)
21.
Halbwachs, N., Péron, M.: Discovering properties about arrays in simple programs. ACM SIGPLAN Not. 43, 339–348 (2008)CrossRef
22.
Horwitz, S., Reps, T., Binkley, D.: Interprocedural slicing using dependence graphs. ACM Trans. Program. Lang. Syst. 12, 26–60 (1990)CrossRef
23.
24.
Jana, A., Khedker, U.P., Datar, A., Venkatesh, R.: Scaling bounded model checking by transforming programs with arrays. CoRR, arXiv:​1606.​06974 (2016)
25.
Khare, S., Saraswat, S., Kumar, S.: Static program analysis of large embedded code base: an experience. In: ISEC (2011)
26.
Kroening, D., Lewis, M., Weissenbacher, G.: Under-approximating loops in C programs for fast counterexample detection. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 381–396. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-39799-8_​26 CrossRef
27.
Liu, J., Rival, X.: Abstraction of arrays based on non contiguous partitions. In: D’Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 282–299. Springer, Heidelberg (2015). doi:10.​1007/​978-3-662-46081-8_​16
28.
29.
Metadaten
Titel
Scaling Bounded Model Checking by Transforming Programs with Arrays
verfasst von
Anushri Jana
Uday P. Khedker
Advaita Datar
R. Venkatesh
Niyas C.
Copyright-Jahr
2017
Buch
Logic-Based Program Synthesis and Transformation

Print ISBN: 978-3-319-63138-7

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

Copyright-Jahr: 2017

DOI
https://doi.org/10.1007/978-3-319-63139-4_16

Premium Partner

    Bildnachweise