Advertisement

An SMT-Based Approach to Coverability Analysis

  • Javier Esparza
  • Ruslán Ledesma-Garza
  • Rupak Majumdar
  • Philipp Meyer
  • Filip Niksic
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8559)

Abstract

Model checkers based on Petri net coverability have been used successfully in recent years to verify safety properties of concurrent shared-memory or asynchronous message-passing software. We revisit a constraint approach to coverability based on classical Petri net analysis techniques. We show how to utilize an SMT solver to implement the constraint approach, and additionally, to generate an inductive invariant from a safety proof. We empirically evaluate our procedure on a large set of existing Petri net benchmarks. Even though our technique is incomplete, it can quickly discharge most of the safe instances. Additionally, the inductive invariants computed are usually orders of magnitude smaller than those produced by existing solvers.

Keywords

Model Checker Coverability Analysis Mutual Exclusion Satisfying Assignment Integer Arithmetic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    Bouajjani, A., Emmi, M.: Bounded phase analysis of message-passing programs. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 451–465. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  2. 2.
    de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  3. 3.
    Delzanno, G., Raskin, J.-F., Van Begin, L.: Towards the automated verification of multithreaded java programs. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 173–187. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  4. 4.
    D’Osualdo, E., Kochems, J., Ong, C.-H.L.: Automatic verification of Erlang-style concurrency. In: Logozzo, F., Fähndrich, M. (eds.) Static Analysis. LNCS, vol. 7935, pp. 454–476. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  5. 5.
    Esparza, J., Melzer, S.: Verification of safety properties using integer programming: Beyond the state equation. Formal Methods in System Design 16(2), 159–189 (2000)CrossRefGoogle Scholar
  6. 6.
    Ganty, P., Majumdar, R.: Algorithmic verification of asynchronous programs. ACM Trans. Program. Lang. Syst. 34(1), 6 (2012)CrossRefGoogle Scholar
  7. 7.
    Ganty, P., Raskin, J.-F., Van Begin, L.: From many places to few: Automatic abstraction refinement for Petri nets. Fundam. Inform. 88(3), 275–305 (2008)zbMATHGoogle Scholar
  8. 8.
    Geeraerts, G., Raskin, J.-F., Begin, L.V.: Expand, enlarge and check: New algorithms for the coverability problem of WSTS. J. Comput. Syst. Sci. 72(1), 180–203 (2006)CrossRefzbMATHGoogle Scholar
  9. 9.
    German, S.M., Sistla, A.P.: Reasoning about systems with many processes. Journal of the ACM (JACM) 39(3), 675–735 (1992)CrossRefzbMATHMathSciNetGoogle Scholar
  10. 10.
    Kaiser, A., Kroening, D., Wahl, T.: Dynamic cutoff detection in parameterized concurrent programs. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 645–659. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  11. 11.
    Kaiser, A., Kroening, D., Wahl, T.: Efficient coverability analysis by proof minimization. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 500–515. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  12. 12.
    Karp, R., Miller, R.: Parallel program schemata. J. Comput. Syst. Sci. 3(2), 147–195 (1969)CrossRefzbMATHMathSciNetGoogle Scholar
  13. 13.
    Kloos, J., Majumdar, R., Niksic, F., Piskac, R.: Incremental, inductive coverability. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 158–173. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  14. 14.
    Lamport, L.: The mutual exclusion problem: Part II—statement and solutions. J. ACM 33(2), 327–348 (1986)CrossRefzbMATHMathSciNetGoogle Scholar
  15. 15.
    Majumdar, R., Meyer, R., Wang, Z.: Static provenance verification for message passing programs. In: Logozzo, F., Fähndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 366–387. Springer, Heidelberg (2013)Google Scholar
  16. 16.
    Murata, T.: Petri nets: Properties, analysis and applications. Proceedings of the IEEE 77(4), 541–580 (1989)CrossRefGoogle Scholar
  17. 17.
    Rackoff, C.: The covering and boundedness problems for vector addition systems. Theor. Comput. Sci. 6, 223–231 (1978)CrossRefzbMATHMathSciNetGoogle Scholar
  18. 18.
    Reisig, W.: Understanding Petri Nets - Modeling Techniques, Analysis Methods, Case Studies. Springer (2013)Google Scholar
  19. 19.
    Schrijver, A.: Theory of Linear and Integer Programming. John Wiley & Sons Ltd. (1986)Google Scholar
  20. 20.
    Solar-Lezama, A., Tancau, L., Bodík, R., Seshia, S., Saraswat, V.: Combinatorial sketching for finite programs. In: ASPLOS, pp. 404–415. ACM (2006)Google Scholar
  21. 21.
    Valmari, A., Hansen, H.: Old and new algorithms for minimal coverability sets. In: Haddad, S., Pomello, L. (eds.) PETRI NETS 2012. LNCS, vol. 7347, pp. 208–227. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  22. 22.
    Wimmel, H., Wolf, K.: Applying CEGAR to the Petri net state equation. Logical Methods in Computer Science 8(3) (2012)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Javier Esparza
    • 1
  • Ruslán Ledesma-Garza
    • 1
  • Rupak Majumdar
    • 2
  • Philipp Meyer
    • 1
  • Filip Niksic
    • 2
  1. 1.Technische Universität MünchenGermany
  2. 2.Max Planck Institute for Software Systems (MPI-SWS)Germany

Personalised recommendations