Local proofs for global safety properties. (English) Zbl 1176.68118
Summary: This paper explores locality in proofs of global safety properties of concurrent programs. Model checking on the full state space is often infeasible due to state explosion. A local proof, in contrast, is a collection of per-process invariants, which together imply the desired global safety property. Local proofs can be more compact than global proofs, but local reasoning is also inherently incomplete. In this paper, we present an algorithm for safety verification that combines local reasoning with gradual refinement. The algorithm gradually exposes facts about the internal state of components, until either a local proof or a real error is discovered. The refinement mechanism ensures completeness. Experiments show that local reasoning can have significantly better performance over the traditional reachability computation. Moreover, for some parameterized protocols, a local proof can be used as the basis of a correctness proof over all instances.
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
Software:
CESARReferences:
| [1] | Balaban I, Fang Y, Pnueli A, Zuck LD (2005) IIV: An invisible invariant verifier. In: CAV. LNCS, vol 3576. Springer, Berlin, pp 408–412 · Zbl 1081.68603 |
| [2] | Chaki S, Clarke EM, Sinha N, Thati P (2005) Automated assume-guarantee reasoning for simulation conformance. In: CAV. LNCS, vol 3576. Springer, Berlin, pp 534–547 · Zbl 1081.68612 |
| [3] | Chandy KM, Misra J (1981) Proofs of networks of processes. IEEE Trans Softw Eng 7(4):417–426 · doi:10.1109/TSE.1981.230844 |
| [4] | Clarke EM, Grumberg O (1987) Avoiding the state explosion problem in temporal logic model checking. In: PODC, pp 294–303 |
| [5] | Clarke EM, Grumberg O, Jha S, Lu Y, Veith H (2003) Counterexample-guided abstraction refinement for symbolic model checking. J Assoc Comput Mach 50(5):752–794 · Zbl 1325.68145 |
| [6] | Clarke EM, Emerson EA (1981) Design and synthesis of synchronization skeletons using branching time temporal logic. In: Workshop on logics of programs. LNCS, vol 131. Springer, Berlin |
| [7] | Cobleigh JM, Avrunin GS, Clarke LA (2006) Breaking up is hard to do: an investigation of decomposition for assume-guarantee reasoning. In: ISSTA, pp 97–108 |
| [8] | Cohen A, Namjoshi KS (2008) Local proofs for linear-time properties of concurrent programs. In: CAV (to appear) · Zbl 1155.68363 |
| [9] | Cousot P, Cousot R (1984) Invariance proof methods and analysis techniques for parallel programs. In: Biermann AW, Guiho G, Kadratoff Y (eds) Automatic program construction techniques. Macmillan, New York, pp 243–271, chap 12 |
| [10] | de Roever W-P, de Boer F, Hannemann U, Hooman J, Lakhnech Y, Poel M, Zwiers J (2001) Concurrency verification: introduction to compositional and noncompositional proof methods. Cambridge University Press, Cambridge · Zbl 1009.68020 |
| [11] | Dijkstra EW (1976) A discipline of programming. Prentice Hall, New York · Zbl 0368.68005 |
| [12] | Dijkstra EW (1976) EWD 554: A Personal Summary of the Gries-Owicki Theory. Available at http://www.cs.utexas.edu/users/EWD |
| [13] | Dijkstra EW, Scholten CS (1990) Predicate calculus and program semantics. Springer, Berlin · Zbl 0698.68011 |
| [14] | Flanagan C, Freund SN, Qadeer S, Seshia SA (2005) Modular verification of multithreaded programs. Theor Comput Sci 338(1–3):153–183 · Zbl 1108.68080 · doi:10.1016/j.tcs.2004.12.006 |
| [15] | Flanagan C, Qadeer S (2003) Thread-modular model checking. In: SPIN. LNCS, vol 2648. Springer, Berlin, pp 213–224 · Zbl 1023.68529 |
| [16] | Giannakopoulou D, Pasareanu CS (2005) Learning-based assume-guarantee verification (tool paper). In: SPIN. LNCS, vol 3639. Springer, Berlin, pp 282–287 |
| [17] | Giannakopoulou D, Pasareanu CS, Barringer H (2002) Assumption generation for software component verification. In: ASE, pp 3–12 |
| [18] | Henzinger TA, Jhala R, Majumdar R (2004) Race checking by context inference. In: PLDI, pp 1–13 |
| [19] | Henzinger TA, Jhala R, Majumdar R, Qadeer S (2003) Thread-modular abstraction refinement. In: CAV. LNCS, vol 2725. Springer, Berlin, pp 262–274 · Zbl 1278.68175 |
| [20] | Hu AJ, Dill DL (1993) Efficient verification with bdds using implicitly conjoined invariants. In: CAV. LNCS, vol 697. Springer, Berlin, pp 3–14 |
| [21] | Jhala R, McMillan KL (2001) Microarchitecture verification by compositional model checking. In: CAV. LNCS, vol 2102. Springer, Berlin, pp 396–410 · Zbl 0991.68639 |
| [22] | Jones CB (1981) Development methods for computer programs including a notion of interference. PhD thesis, Oxford University |
| [23] | Lamport L (1977) Proving the correctness of multiprocess programs. IEEE Trans Softw Eng 3(2):125–143 · doi:10.1109/TSE.1977.229904 |
| [24] | Malkis A, Podelski A, Rybalchenko A (2007) Precise thread-modular verification. In: SAS, pp 218–232 · Zbl 1211.68095 |
| [25] | McMillan KL (1997) A compositional rule for hardware design refinement. In: CAV. LNCS, vol 1254. Springer, Berlin |
| [26] | Namjoshi KS (2007) Symmetry and completeness in the analysis of parameterized systems. In: VMCAI. LNCS, vol 4349. Springer, Berlin · Zbl 1132.68476 |
| [27] | Owicki SS, Gries D (1976) Verifying properties of parallel programs: An axiomatic approach. Commun Assoc Comput Mach 19(5):279–285 · Zbl 0322.68010 |
| [28] | Pnueli A (1985) In transition from global to modular reasoning about programs. In: Logics and models of concurrent systems. NATO ASI series · Zbl 0578.68014 |
| [29] | Pnueli A, Ruah S, Zuck LD (2001) Automatic deductive verification with invisible invariants. In: TACAS. LNCS, vol 2031. Springer, Berlin, pp 82–97 · Zbl 0978.68539 |
| [30] | Pnueli A, Shahar E (1996) A platform for combining deductive with algorithmic verification. In: CAV. LNCS, vol 1102. Springer, Berlin, pp 184–195. Web: www.cs.nyu.edu/acsys/tlv |
| [31] | Queille JP, Sifakis J (1982) Specification and verification of concurrent systems in CESAR. In: Proc of the 5th international symposium on programming. LNCS, vol 137. Springer, Berlin · Zbl 0482.68028 |
| [32] | Shoham S, Grumberg O (2007) Compositional verification and 3-valued abstractions join forces. In: SAS, pp 69–86 · Zbl 1211.68256 |
| [33] | Tkachuk O, Dwyer MB, Pasareanu CS (2003) Automated environment generation for software model checking. In: ASE, pp 116–129 |
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
