Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Bringing LTL Model Checking to Biologists Read chapter Read first chapter

2017 | OriginalPaper | Chapter

Dynamic Reductions for Model Checking Concurrent Software

Authors : Henning Günther, Alfons Laarman, Ana Sokolova, Georg Weissenbacher

Published in: Verification, Model Checking, and Abstract Interpretation

Publisher: Springer International Publishing

Log in

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

search-config
loading …

Abstract

Symbolic model checking of parallel programs stands and falls with effective methods of dealing with the explosion of interleavings. We propose a dynamic reduction technique to avoid unnecessary interleavings. By extending Lipton’s original work with a notion of bisimilarity, we accommodate dynamic transactions, and thereby reduce dependence on the accuracy of static analysis, which is a severe bottleneck in other reduction techniques.
The combination of symbolic model checking and dynamic reduction techniques has proven to be challenging in the past. Our generic reduction theorem nonetheless enables us to derive an efficient symbolic encoding, which we implemented for IC3 and BMC. The experiments demonstrate the power of dynamic reduction on several case studies and a large set of SVCOMP benchmarks.

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
previous chapter Stabilizing Floating-Point Programs Using Provenance Analysis
next chapter Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games
Literature
1.
Alur, R., Brayton, R.K., Henzinger, T.A., Qadeer, S., Rajamani, S.K.: Partial-order reduction in symbolic state space exploration. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 340–351. Springer, Heidelberg (1997). doi:10.​1007/​3-540-63166-6_​34 CrossRef
2.
3.
Beyer, D.: Reliable and reproducible competition results with benchexec and witnesses (Report on SV-COMP 2016). In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 887–904. Springer, Heidelberg (2016). doi:10.​1007/​978-3-662-49674-9_​55 CrossRef
4.
Beyer, D., Cimatti, A., Griggio, A., Erkan Keremoglu, M., Sebastiani, R.: Software model checking via large-block encoding. In: FMCAD, pp. 25–32. IEEE (2009)
5.
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
6.
Birgmeier, Johannes, Bradley, Aaron, R., Weissenbacher, Georg: Counterexample to induction-guided abstraction-refinement (CTIGAR). In: Biere, Armin, Bloem, Roderick (eds.) CAV 2014. LNCS, vol. 8559, pp. 831–848. Springer, Cham (2014). doi:10.​1007/​978-3-319-08867-9_​55
7.
Bondy, J.A., Murty, U.S.R.: Graph Theory with Applications, vol. 290. Macmillan, London (1976)CrossRefMATH
8.
9.
Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: IC3 modulo theories via implicit predicate abstraction. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 46–61. Springer, Heidelberg (2014). doi:10.​1007/​978-3-642-54862-8_​4 CrossRef
10.
11.
Dimitrov, D., et al.: Commutativity race detection. ACM SIGPLAN Not. 49(6), 305–315 (2014)CrossRef
12.
Doeppner Jr., T.W.: Parallel program correctness through refinement. In: POPL, pp. 155–169. ACM (1977)
13.
Dwyer, M.B., Robby, J.H., Ranganath, V.P.: Exploiting object escape, locking information in partial-order reductions for concurrent object-oriented programs. FMSD 25(2–3), 199–240 (2004)MATH
14.
Elmas, T., Qadeer, S., Tasiran, S.: A calculus of atomic actions. In: POPL, pp. 2–15. ACM (2009)
15.
Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: POPL, vol. 40, no. 1, pp. 110–121. ACM (2005)
16.
Flanagan, C., Qadeer, S.: Transactions for software model checking. ENTCS 89(3), 518–539 (2003). Software Model CheckingMATH
17.
Flanagan, C., Qadeer, S.: A type and effect system for atomicity. In: PLDI, pp. 338–349. ACM (2003)
18.
19.
Godefroid, P. (ed.): Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol. 1032. Springer, Heidelberg (1996)MATH
20.
21.
Grumberg, O., Lerda, F., Strichman, O., Theobald, M.: Proof-guided under approximation-widening for multi-process systems. In: POPL, pp. 122–131. ACM (2005)
22.
23.
24.
Günther, H., Laarman, A., Weissenbacher, G.: Vienna verification tool: IC3 for parallel software. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 954–957. Springer, Heidelberg (2016). doi:10.​1007/​978-3-662-49674-9_​69 CrossRef
25.
Günther, H., Weissenbacher, G.: Incremental bounded software model checking. In: SPIN, pp. 40–47. ACM (2014)
26.
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL, pp. 58–70. ACM (2002)
27.
Kahlon, V., Gupta, A., Sinha, N.: Symbolic model checking of concurrent programs using partial orders and on-the-fly transactions. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 286–299. Springer, Heidelberg (2006). doi:10.​1007/​11817963_​28 CrossRef
28.
Kahlon, V., Wang, C., Gupta, A.: Monotonic partial order reduction: an optimal symbolic partial order reduction technique. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 398–413. Springer, Heidelberg (2009). doi:10.​1007/​978-3-642-02658-4_​31 CrossRef
29.
Kurshan, R., Levin, V., Minea, M., Peled, D., Yenigün, H.: Static partial order reduction. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 345–357. Springer, Heidelberg (1998). doi:10.​1007/​BFb0054182 CrossRef
30.
Laarman, A.W., van de Pol, J.C., Weber, M.: Boosting multi-core reachability performance with shared hash tables. In: FMCAD, pp. 247–255. IEEE-CS (2010)
31.
Lamport, L., Schneider, F.B.: Pretending atomicity. Technical report, Cornell University (1989)
32.
33.
34.
Milner, R.: Communication and Concurrency. Prentice Hall, New York (1989)MATH
35.
Nalumasu, R., Gopalakrishnan, G.: An efficient partial order reduction algorithm with an alternative proviso implementation. FMSD 20(3), 231–247 (2002)MATH
36.
Papadimitriou, C.: The Theory of Database Concurrency Control. Principles of Computer Science Series. Computer Science Press, San Jose (1986)MATH
37.
Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167–183. Springer, Berlin, Heidelberg (1981). doi:10.​1007/​BFb0017309 CrossRef
38.
39.
Popeea, C., Rybalchenko, A., Wilhelm, A.: Reduction for compositional verification of multi-threaded programs. In: FMCAD, pp. 187–194. IEEE (2014)
40.
Stoller, S.D., Cohen, E.: Optimistic synchronization-based state-space reduction. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 489–504. Springer, Heidelberg (2003). doi:10.​1007/​3-540-36577-X_​36 CrossRef
41.
Valmari, A.: Eliminating redundant interleavings during concurrent program verification. In: Odijk, E., Rem, M., Syre, J.-C. (eds.) PARLE 1989. LNCS, vol. 366, pp. 89–103. Springer, Heidelberg (1989). doi:10.​1007/​3-540-51285-3_​35 CrossRef
42.
43.
Metadata
Title
Dynamic Reductions for Model Checking Concurrent Software
Authors
Henning Günther
Alfons Laarman
Ana Sokolova
Georg Weissenbacher
Copyright Year
2017
Book
Verification, Model Checking, and Abstract Interpretation

Print ISBN: 978-3-319-52233-3

Electronic ISBN: 978-3-319-52234-0

Copyright Year: 2017

DOI
https://doi.org/10.1007/978-3-319-52234-0_14

Premium Partner

    Image Credits