LNCS 2772 - Counterexamples Revisited: Principles ...

1 Counterexamples Revisited: Principles , Algorithms, Applications Edmund Clarke1and Helmut Veith21 School of Computer Science, Carnegie Mellon University, f ur Informationsysteme, Technische Universit at Wien, counterexample generation is a central featureof model checking which sets the method apart from other approachessuch as theorem proving. The practical value of Counterexamples tothe verification engineer is evident, and for many years, counterexam-ple generation algorithms have been employed in model checking sys-tems, even though they had not been subject to an adequate fundamen-tal investigation. Recent advances in model checking technology suchas counterexample-guided abstraction refinement have put strong em-phasis on Counterexamples , and have lead to renewed interest both infundamental and pragmatic aspects of counterexample generation.

2 Inthis paper, we survey several key contributions to the subject includ-ing symbolic algorithms, results about the graph-theoretic structure ofcounterexamples, and applications to automated abstraction as well assoftware is not a virtue of a theory (as people often think) but a R. Popper1 IntroductionDisproof by counterexample is an ancient mathematical concept which lends it-self naturally to refute universal statements. Formally, a counterexample to a uni-versal formula x (x) is given by a constantcfor which (c) evaluates to their most visible form, mathematical Counterexamples refute long-standing This research was sponsored by the Semiconductor Research Corporation (SRC) un-der contract no. 99-TJ-684, the National Science Foundation (NSF) under grant , the Office of Naval Research (ONR), the Naval Research Laboratory(NRL) under contract no.

3 N00014-01-1-0796, and by the Defense Advanced ResearchProjects Agency, the Army Research Office (ARO) under contract no. DAAD19-01-1-0485, the General Motors Collaborative Research Lab at CMU, the Austrian ScienceFund Project N Z29-N04, and the EU Research and Training Network GAMES. Theviews and conclusions contained in this document are those of the author and shouldnot be interpreted as representing the official policies, either expressed or implied,of SRC, NSF, ONR, NRL, DOD, ARO, or the Dershowitz (Ed.): Verification (Manna Festschrift), LNCS 2772, pp. 208 224, Springer-Verlag Berlin Heidelberg 2003 Counterexamples Revisited: Principles , Algorithms, Applications209conjectures, but much more often, Counterexamples are natural byproducts inthe early stages of a mathematical analysis; they typically exhibit pathologicalcases, refining our techniques and helping to shape the definitions we formal verification, the situation is similar.

4 The specifications for a system a piece of hardware or software essentially amount to conjectures about aformal model of the system; although the specifications are expected to be true,there is a need for a systematic way to check for specification violations, andsubstantiate possible violations by concrete Counterexamples . Experience hasshown that Counterexamples are the single most effective feature to convincesystem engineers about the value of formal checking [20,15,52] is an algorithmic framework tailored to performthis verification task; on a high level, model checking can be viewed as an ex-haustive search algorithm which exploits various optimization strategies to finda counterexample. Consequently, it is possible, at least in principle, to have amodel checker systematically output Counterexamples for violated practically successful model checkers including SMV [48,10,20] are able tooutput Counterexamples in varying formats, cf.

5 Figure of a hardware main practical problem in model checking is the combinatorial explo-sion of system states commonly known as thestate explosion explosion problem which renders apparently good theoretical results suchas linear time model checking algorithms practically pointless, because the sys-tem size is so large that linear time is prohibitively expensive in practice. Mostcurrent research in model checking is therefore devoted to combating state explo-sion [18]. The context of the state explosion problem makes the counterexamplefeature even more important, because Counterexamples are often composed onlyof several their practical importance, Counterexamples often have been dealtwith in an ad hoc manner, as if they were only parts of the user interface. Inparticular, they used to be a blind spot in fundamental research until the last few years however, Counterexamples have attracted renewed in-terest; they have been increasingly recognized as data structures worth of aclose algorithmic and logical analysis.

6 This paper puts a spotlight on counterex-amples. We survey theoretical and practical results, and focus in particular onrecent Clarke and Helmut VeithSection 3 deals with fundamental aspects, in particular with the graph-theoretic structure of Counterexamples and their appropriateness for differenttemporal specification Section 4 we demonstrate on two examples how Counterexamples are usedto improve the algorithmic efficiency of verification procedures. We first arguethat bounded model checking can be viewed as a parameterized counterexam-ple construction. Second, we present the CEGAR (Counterexample-Guided Ab-straction Refinement) framework, various instantiations of which are used instate-of-the-art model checking Section 5 we survey user-oriented applications of Counterexamples in dif-ferent frameworks, most notably in software verification, where ordinary coun-terexamples are only part of a more complex debugging Temporal Logic model checking in a NutshellA model checking system usually comes with a specialized compiler which trans-lates the system description into a data structure representing a Kripke struc-ture.

7 Given a setPof atomic propositions, a Kripke structure overPis a tupleK=(S, I, R, L), whereSis a finite set of states,I Sis the set of initial states,R S Sis a total transition relation, andL:S 2 Pis a function that labelseach state with a set of atomic =s0,s1,s2, ..starting at statesis an infinite sequence of statessuch thats=s0and (si,si+1) Rfor alli nto denote thesuffix of that begins at statesn,and (n)to denote the statesnon .Whenthe context is clear, nsometimes is also used to denote the state (n).WewritePaths(s) to denote the set of paths starting at are expressed in terms of temporal logics such as CTL or LTL.(Note that the notation for CTL by Clarke and Emerson [15] was inspired bythe paper [5] by Ben-Ari, Manna, and Pnueli.) CTL is the logic obtained frompropositional logic by introducing the unary modalitiesX, G, F, E, Aand thebinary modalityU.

8 State formulas and path formulas are defined inductivelyas follows: (i) Atomic formulas are state formulas. (ii) All state formulas arepath formulas. (iii) State formulas are closed under conjunction, disjunction,and negation. (iv) If and are state formulas, thenX ,G ,F and U are path formulas. (v) If is a path formula, thenE andA are state semantics of CTL is defined in Figure 2. When it is clear from the context,we will |= to denoteK, s0|= ,wheres0is the uniqueinitial state time logic LTL is the fragment of CTL where each formula has theformA where does not containAandE. CTL is the fragment of CTL whereeach path operatorX, F, G, Uis immediately preceded by eitherEorA, ,temporal operators only occur in the compound formEX, EG, EF, EU, AX,AG, AF, AU. ACTL is the fragment of CTL whereEdoes not occur, andnegation is restricted to atomic subformulas.

9 ACTL is the analogous fragmentof CTL. We shall call ACTL, ACTL and LTLuniversal fragmentsof CTL . Counterexamples Revisited: Principles , Algorithms, Applications211K, s|=p: p L(s)K, |= 1: K, (0)|= 1K, s|= 1: K, s |= 1K, s|= 1 2: K, s|= 1andK, s|= 2K, s|= 1 2: K, s|= 1orK, s|= 2K, |=X 1: K, 1|= 1K, |=G 1: i , i|= 1K, |=F 1: i , i|= 1K, |= 1U 2: n N i< , i|= 1andK, n|= 2K, s|=E 1: Paths(s).K, |= 1K, s|=A 1: Paths(s).K, |= 1 Fig. of CTL , assuming that 1and 2are state formulas, andthat 1and 2are path model checking problem for a logic L is to decide if for givenK, sand Lit holds thatK, s|= . For CTL and LTL, this problem is PSPACE-complete [56], while for CTL, the time complexity is linear in the size of bothKand . Note that due to state explosion, however, the dominant factor in thisanalysis is checking algorithms can be classified intoexplicitandsymbolicalgo-rithms.

10 Symbolic algorithms employ data structures such as Binary Decision Di-agrams [8] to describe sets of states; in many cases, symbolic algorithms achievegreat reductions in the size of the data structures, and thus help to alleviatethe state explosion problem [10]. Explicit algorithms in contrast are algorithmswhich work directly on the Kripke structure, and construct necessary parts ofthe Kripke structure on the fly, using methods such as partial order reduction toprune the search space. Traditionally, symbolic methods have been used primar-ily for CTL, while explicit methods are typical of LTL model checking . Examplesof symbolic and explicit model checkers are SMV [48,11,20] and SPIN [38,39] What Is a Counterexample?Suppose that your favorite model checking tool determines that the specification is violated over Kripke structureK, ,K |=.