Skip to main content

2017 | OriginalPaper | Buchkapitel

CPA-BAM-BnB: Block-Abstraction Memoization and Region-Based Memory Models for Predicate Abstractions

(Competition Contribution)

verfasst von : Pavel Andrianov, Karlheinz Friedberger, Mikhail Mandrykin, Vadim Mutilin, Anton Volkov

Erschienen in: Tools and Algorithms for the Construction and Analysis of Systems

Verlag: Springer Berlin Heidelberg

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

search-config
loading …

Abstract

Our submission to SV-COMP’17 is based on the software verification framework CPAchecker. Combined with value analysis and predicate analysis we use the concept of block-abstraction memoization with optimization and several fixes relative to the version of SV-COMP’16. A novelty of our approach is usage of BnB memory model for predicate analysis, which efficiently divides the accessed memory into memory regions and thus leads to smaller formulas.

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!

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!

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!

Literatur
1.
Zurück zum Zitat Beyer, D., Henzinger, T.A., Théoduloz, G.: Configurable software verification: concretizing the convergence of model checking and program analysis. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 504–518. Springer, Heidelberg (2007). doi:10.1007/978-3-540-73368-3_51 CrossRef Beyer, D., Henzinger, T.A., Théoduloz, G.: Configurable software verification: concretizing the convergence of model checking and program analysis. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 504–518. Springer, Heidelberg (2007). doi:10.​1007/​978-3-540-73368-3_​51 CrossRef
2.
Zurück zum Zitat Karpenkov, E.G., Friedberger, K., Beyer, D.: JavaSMT: a unified interface for SMT solvers in java. In: Blazy, S., Chechik, M. (eds.) VSTTE 2016. LNCS, vol. 9971, pp. 139–148. Springer, Heidelberg (2016). doi:10.1007/978-3-319-48869-1_11 CrossRef Karpenkov, E.G., Friedberger, K., Beyer, D.: JavaSMT: a unified interface for SMT solvers in java. In: Blazy, S., Chechik, M. (eds.) VSTTE 2016. LNCS, vol. 9971, pp. 139–148. Springer, Heidelberg (2016). doi:10.​1007/​978-3-319-48869-1_​11 CrossRef
3.
4.
Zurück zum Zitat Friedberger, K.: CPA-BAM: block-abstraction memoization with value analysis and predicate analysis. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 912–915. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49674-9_58 CrossRef Friedberger, K.: CPA-BAM: block-abstraction memoization with value analysis and predicate analysis. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 912–915. Springer, Heidelberg (2016). doi:10.​1007/​978-3-662-49674-9_​58 CrossRef
5.
Zurück zum Zitat Bornat, R.: Proving pointer programs in Hoare logic. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol. 1837, pp. 102–126. Springer, Heidelberg (2000). doi:10.1007/10722010_8 CrossRef Bornat, R.: Proving pointer programs in Hoare logic. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol. 1837, pp. 102–126. Springer, Heidelberg (2000). doi:10.​1007/​10722010_​8 CrossRef
6.
Zurück zum Zitat Burstall, R.M.: Some techniques for proving correctness of programs which alter data structures. Mach. Intell. 7, 23–50 (1972)MATH Burstall, R.M.: Some techniques for proving correctness of programs which alter data structures. Mach. Intell. 7, 23–50 (1972)MATH
7.
Zurück zum Zitat Löwe, S., Mandrykin, M., Wendler, P.: CPAchecker with sequential combination of explicit-value analyses and predicate analyses. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 392–394. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54862-8_27 CrossRef Löwe, S., Mandrykin, M., Wendler, P.: CPAchecker with sequential combination of explicit-value analyses and predicate analyses. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 392–394. Springer, Heidelberg (2014). doi:10.​1007/​978-3-642-54862-8_​27 CrossRef
Metadaten
Titel
CPA-BAM-BnB: Block-Abstraction Memoization and Region-Based Memory Models for Predicate Abstractions
verfasst von
Pavel Andrianov
Karlheinz Friedberger
Mikhail Mandrykin
Vadim Mutilin
Anton Volkov
Copyright-Jahr
2017
Verlag
Springer Berlin Heidelberg
DOI
https://doi.org/10.1007/978-3-662-54580-5_22