Context-aware counter abstraction

Ball T, Rajamani SK (2000) Bebop: a symbolic model checker for Boolean programs. In: SPIN, pp 113–130

Ball T, Rajamani SK (2002) The SLAM project: debugging system software via static analysis. In: POPL, pp 1–3

Ball T, Chaki S, Rajamani SK (2001) Parameterized verification of multithreaded software libraries. In: TACAS, pp 158–173

Ball T, Bounimova E, Cook B, Levin V, Lichtenberg J, McGarvey C, Ondrusek B, Rajamani SK, Ustuner A (2006) Thorough static analysis of device drivers. In: EuroSys, pp 73–85

Barner S, Grumberg O (2005) Combining symmetry reduction and under-approximation for symbolic Model Checking. Form Methods Syst Des 27(1–2):29–66

Basler G, Mazzucchi M, Wahl T, Kroening D (2009) Symbolic counter abstraction for concurrent software. In: CAV, pp 64–78

Bosnacki D, Dams D, Holenderski L (2002) Symmetric spin. Int J Softw Tools Technol Transf 4(1):92–106

Clarke EM, Jha S, Enders R, Filkorn T (1996) Exploiting symmetry in temporal logic Model Checking. Form Methods Syst Des 9(1/2):77–104

Clarke EM, Kroening D, Sharygina N, Yorav K (2005) SATABS: SAT-based predicate abstraction for ANSI-C. In: TACAS, pp 570–574

Cook B, Kroening D, Sharygina N (2005) Symbolic Model Checking for asynchronous Boolean programs. In: SPIN, pp 75–90

Cook B, Kroening D, Sharygina N (2007) Verification of Boolean programs with unbounded thread creation. Theor Comput Sci 388(13):227–242

Delzanno G (2000) Automatic verification of parameterized cache coherence protocols. In: CAV, pp 53–68

Donaldson AF, Miller A (2006) Exact and approximate strategies for symmetry reduction in model checking. In: FM, pp 541–556

Donaldson AF, Miller A (2006) Symmetry reduction for probabilistic Model Checking using generic representatives. In: ATVA, pp 9–23

Donaldson A, Miller A, Parker D (2009) Language-level symmetry reduction for probabilistic Model Checking. In: QEST, pp 289–298

Emerson EA, Sistla AP (1996) Symmetry and Model Checking. Form Methods Syst Des 9(1/2):105–131

Emerson EA, Trefler RJ (1999) From asymmetry to full symmetry: new techniques for symmetry reduction in Model Checking. In: CHARME, pp 142–156

Emerson EA, Wahl T (2005) Dynamic symmetry reduction. In: TACAS, pp 382–396

Emerson EA, Wahl T (2005) Efficient reduction techniques for systems with many components. Electron Notes Theor Comput Sci 130:379–399

Emerson EA, Jha S, Peled D (1997) Combining partial order and symmetry reductions. In: TACAS, pp 19–34

Emerson EA, Havlicek J, Trefler RJ (2000) Virtual symmetry reduction. In: LICS, pp 121–131

Flanagan C, Godefroid P (2005) Dynamic partial-order reduction for Model Checking software. In: POPL, pp 110–121

Graf S, Saïdi H (1997) Construction of abstract state graphs with PVS. In: CAV, pp 72–83

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

Holzmann GJ, Peled D (1994) An improvement in formal verification. In: FORTE, pp 197–211

Kurshan RP (1994) Computer-aided verification of coordinating processes: the automata-theoretic approach. Princeton University Press, Princeton

Lahiri SK, Bryant RE, Cook B (2003) A symbolic approach to predicate abstraction. In: CAV, pp 141–153

Lubachevsky BD (1984) An approach to automating the verification of compact parallel coordination programs I. Acta Inform 21:125–169

Manevich R, Lev-Ami T, Sagiv M, Ramalingam G, Berdine J (2008) Heap decomposition for concurrent shape analysis. In: SAS, pp 363–377

Melton R, Dill D Murφ annotated reference manual, rel. 3.1. http://verify.stanford.edu/dill/murphi.html

Pnueli A, Xu J, Zuck LD (2002) Liveness with (0,1,∞)-counter abstraction. In: CAV, pp 107–122

Pong F, Dubois M (1995) A new approach for the verification of cache coherence protocols. IEEE Trans Parallel Distrib Syst 6(8):773–787

Somenzi F The CU decision diagram package, release 2.3.1. University of Colorado at Boulder. http://vlsi.colorado.edu/~fabio/CUDD/

Suwimonteerabuth D, Esparza J, Schwoon S (2008) Symbolic context-bounded analysis of multithreaded java programs. In: SPIN, pp 270–287

Wahl T, Blanc N, Emerson EA (2008) SVISS: symbolic verification of symmetric systems. In: TACAS, pp 459–462

Wei O, Gurfinkel A, Chechik M (2005) Identification and counter abstraction for full virtual symmetry. In: CHARME, pp 285–300

Witkowski T, Blanc N, Kroening D, Weissenbacher G (2007) Model Checking concurrent Linux device drivers. In: ASE, pp 501–504