×

Distributed and predictable software model checking. (English) Zbl 1317.68121

Jhala, Ranjit (ed.) et al., Verification, model checking, and abstract interpretation. 12th international conference, VMCAI 2011, Austin, TX, USA, January 23–25, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-18274-7/pbk). Lecture Notes in Computer Science 6538, 340-355 (2011).
Summary: We present a predicate abstraction and refinement-based algorithm for software verification that is designed for the distributed execution on compute nodes that communicate via message passing, as found in today’s compute clusters. A successful adaptation of predicate abstraction and refinement from sequential to distributed setting needs to address challenges imposed by the inherent non-determinism present in distributed computing environments. In fact, our experiments show that up to an order of magnitude variation of the running time is common when a naive distribution scheme is applied, often resulting in significantly worse running time than the non-distributed version. We present an algorithm that overcomes this pitfall by making deterministic the counterexample selection in spite of the distribution, and still efficiently exploits distributed computational resources. We demonstrate that our distributed software verification algorithm is practical by an experimental evaluation on a set of difficult benchmark problems from the transportation domain.
For the entire collection see [Zbl 1206.68013].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Software:

ARMC; SPIN; EigenCFA
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Automatic Verification and Analysis of Complex Systems (AVACS), http://www.avacs.org
[2] Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic Predicate Abstraction of C Programs. In: PLDI (2001)
[3] Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-Guided Abstraction Refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855. Springer, Heidelberg (2000) · Zbl 0974.68517
[4] Cousot, P., Cousot, R.: Abstract Interpretation: a Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In: POPL (1977) · Zbl 1149.68389
[5] Garavel, H., Mateescu, R., Smarandache, I.: Parallel State Space Construction for Model-Checking. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, p. 217. Springer, Heidelberg (2001) · Zbl 0986.68883
[6] Graf, S., Saïdi, H.: Construction of Abstract State Graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, Springer, Heidelberg (1997)
[7] Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from Proofs. In: POPL (2004) · Zbl 1325.68147
[8] Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy Abstraction. In: POPL (2002) · Zbl 1323.68374
[9] Heyman, T., Geist, D., Grumberg, O., Schuster, A.: Achieving Scalability in Parallel Reachability Analysis of Very Large Circuits. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855. Springer, Heidelberg (2000) · Zbl 0974.68547
[10] Holzmann, G.J., Joshi, R., Groce, A.: Tackling Large Verification Problems with the Swarm Tool. In: Havelund, K., Majumdar, R. (eds.) SPIN 2008. LNCS, vol. 5156, pp. 134–143. Springer, Heidelberg (2008) · Zbl 05372758
[11] Jha, S.K.: d-IRA: A Distributed Reachability Algorithm for Analysis of Linear Hybrid Automata. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 618–621. Springer, Heidelberg (2008) · Zbl 1144.93310
[12] Jhala, R., Majumdar, R.: Software Model Checking. ACM Computing Surveys 41(4) (2009)
[13] Lerda, F., Sisto, R.: Distributed-Memory Model Checking with SPIN. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol. 1680, p. 22. Springer, Heidelberg (1999)
[14] Lopes, N.P., Navarro, J.A., Rybalchenko, A., Singh, A.: Applying Prolog to Develop Distributed Systems. Theory and Practice of Logic Programming 10(4-6), 691–707 (2010) · Zbl 1205.68087
[15] Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, Heidelberg (1995) · Zbl 1288.68169
[16] Monniaux, D.: The Parallel Implementation of the Astrée Static Analyzer. In: APLAS (2005) · Zbl 1159.68378
[17] Podelski, A., Rybalchenko, A.: ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement. In: PADL (2007)
[18] Prabhu, T., Ramalingam, S., Might, M., Hall, M.: EigenCFA: Accelerating flow analysis with GPUs. In: POPL (2011) · Zbl 1284.68195
[19] Rybalchenko, A., Sofronie-Stokkermans, V.: Constraint Solving for Interpolation. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 346–362. Springer, Heidelberg (2007) · Zbl 1132.68480
[20] Stern, U., Dill, D.L.: Parallelizing the Mur{\(\phi\)} Verifier. Formal Methods in System Design 18(2), 117–129 (2001) · Zbl 1001.68073
[21] Venet, A., Brat, G.: Precise and Efficient Static Array Bound Checking for Large Embedded C Programs. In: PLDI (2004)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.