Local proofs for global safety properties

Balaban I, Fang Y, Pnueli A, Zuck LD (2005) IIV: An invisible invariant verifier. In: CAV. LNCS, vol 3576. Springer, Berlin, pp 408–412

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

Chandy KM, Misra J (1981) Proofs of networks of processes. IEEE Trans Softw Eng 7(4):417–426

Clarke EM, Grumberg O (1987) Avoiding the state explosion problem in temporal logic model checking. In: PODC, pp 294–303

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

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

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

Cohen A, Namjoshi KS (2008) Local proofs for linear-time properties of concurrent programs. In: CAV (to appear)

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

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

Dijkstra EW (1976) A discipline of programming. Prentice Hall, New York

Dijkstra EW (1976) EWD 554: A Personal Summary of the Gries-Owicki Theory. Available at http://www.cs.utexas.edu/users/EWD

Dijkstra EW, Scholten CS (1990) Predicate calculus and program semantics. Springer, Berlin

Flanagan C, Freund SN, Qadeer S, Seshia SA (2005) Modular verification of multithreaded programs. Theor Comput Sci 338(1–3):153–183

Flanagan C, Qadeer S (2003) Thread-modular model checking. In: SPIN. LNCS, vol 2648. Springer, Berlin, pp 213–224

Giannakopoulou D, Pasareanu CS (2005) Learning-based assume-guarantee verification (tool paper). In: SPIN. LNCS, vol 3639. Springer, Berlin, pp 282–287

Giannakopoulou D, Pasareanu CS, Barringer H (2002) Assumption generation for software component verification. In: ASE, pp 3–12

Henzinger TA, Jhala R, Majumdar R (2004) Race checking by context inference. In: PLDI, pp 1–13

Henzinger TA, Jhala R, Majumdar R, Qadeer S (2003) Thread-modular abstraction refinement. In: CAV. LNCS, vol 2725. Springer, Berlin, pp 262–274

Hu AJ, Dill DL (1993) Efficient verification with bdds using implicitly conjoined invariants. In: CAV. LNCS, vol 697. Springer, Berlin, pp 3–14

Jhala R, McMillan KL (2001) Microarchitecture verification by compositional model checking. In: CAV. LNCS, vol 2102. Springer, Berlin, pp 396–410

Jones CB (1981) Development methods for computer programs including a notion of interference. PhD thesis, Oxford University

Lamport L (1977) Proving the correctness of multiprocess programs. IEEE Trans Softw Eng 3(2):125–143

Malkis A, Podelski A, Rybalchenko A (2007) Precise thread-modular verification. In: SAS, pp 218–232

McMillan KL (1997) A compositional rule for hardware design refinement. In: CAV. LNCS, vol 1254. Springer, Berlin

Namjoshi KS (2007) Symmetry and completeness in the analysis of parameterized systems. In: VMCAI. LNCS, vol 4349. Springer, Berlin

Owicki SS, Gries D (1976) Verifying properties of parallel programs: An axiomatic approach. Commun Assoc Comput Mach 19(5):279–285

Pnueli A (1985) In transition from global to modular reasoning about programs. In: Logics and models of concurrent systems. NATO ASI series

Pnueli A, Ruah S, Zuck LD (2001) Automatic deductive verification with invisible invariants. In: TACAS. LNCS, vol 2031. Springer, Berlin, pp 82–97

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

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

Shoham S, Grumberg O (2007) Compositional verification and 3-valued abstractions join forces. In: SAS, pp 69–86

Tkachuk O, Dwyer MB, Pasareanu CS (2003) Automated environment generation for software model checking. In: ASE, pp 116–129