Counterexample-Guided Abstraction Refinement
10th International Symposium on Temporal Representation and Reasoning, 2003 and Fourth International Conference on Temporal Logic. Proceedings., 2000 · paper · Computer science
Presents an automatic iterative abstraction-refinement method for model checking, which analyzes spurious counterexamples to refine the abstract model. Implemented in NuSMV, experiments including a large Fujitsu IP core design confirm its effectiveness.
Checked: PDF from cs.cmu.edu, fetched 4 Oct 2026. Page numbers are those of that PDF.
3 findings
Substance Theorem 1 assumes only that "the atomic subformulas [of φ] respect h" but claims (i) "L̂(d̂) is consistent for all abstract states", while L is defined over Atoms(P) (atoms of φ and of all transition-block conditions).
- p. 5 Sec. 2, definition of L and Theorem 1
Let h be an abstraction and φ be an ACTL* specification where the atomic subformulas respect h
Only the authors can say what is right here.
Judge's note: Page 5 checked. The paper defines L(d) = {f ∈ Atoms(P) | d ⊨ f} and L̂(d̂) = ∪_{h(d)=d̂} L(d), and 'consistent' means every d ∈ h^-1(d̂) satisfies every f in L̂(d̂). My reworking: let g ∈ Atoms(P) \ Atoms(φ), and let h(d) = h(e) with d ⊨ g and e ⊭ g. The hypothesis of Theorem 1 still holds, because only the atoms of φ need to respect h. But g ∈ L̂(d̂) and e ⊭ g, so (i) fails as printed. The hypothesis has to cover all of Atoms(P), or the labelling has to be restricted to Atoms(φ). Part (ii) is not affected by this. The initial abstraction in Section 4.1 is designed so that Atoms(P) respect h, so the method itself survives, but the theorem statement is false as written.
Second check: another model agreed
Report a problem with this finding
Substance Theorem 2 with T̂_unwind = ⟨ŝ1,…,ŝi⟩⟨ŝ_{i+1},…,ŝn⟩^min ("the number of unwindings is at most the number of concrete states") is false as printed: non-empty h^-1_path(T̂_unwind) does not imply a concrete loop counterexample.
- p. 10 Sec. 4.2, text before Theorem 2
the number of unwindings can be bounded by
- p. 10 Definition of T_unwind and Theorem 2
Then the following theorem holds.
- p. 13 Fig. 8 and Two-phase Refinement paragraph
A spurious loop counterexample
Only the authors can say what is right here.
Judge's note: I checked the definition and Theorem 2 on p10 and Fig. 8 on p13, and reworked the paper's own Fig. 8. The concrete states are 1̂ = {1} and 2̂ = {2,3}. The arrows are 1→1 (self-loop), 1→3 and 2→1. The paper calls ⟨1̂,2̂⟩^ω spurious. There is no prefix, and min = min(|{1}|, |{2,3}|) = 1, so T̂_unwind = ⟨1̂,2̂⟩. The concrete path 1→3 lies in h^-1_path(T̂_unwind), assuming state 1 is initial, which it must be if 1̂ is the initial abstract state. So (ii) holds while (i) fails. The reviewer's separate example also checks out: s1→a, a→b, b→b, b'→a, with h(b) = h(b') = ŝ3. Here min = 1, the path s1,a,b exists, and there is no concrete cycle through a. With min passes, the pigeonhole step does not force a repeated concrete state; min+1 passes would. The proof is deferred to [7], which is not among the files.
Second check: another model agreed
Report a problem with this finding
Reference or label "A similar approach has been described by Balarin in [2, 15]" cites [15], which is "Y. Lakhnech. personal communication. 2000.", not a work by Balarin.
- p. 3 Introduction, related work
A similar approach has been described by Balarin in [2, 15].
- p. 16 Reference 15
Y. Lakhnech. personal communication. 2000.
Only the authors can say what is right here.
Judge's note: Page 3 sentence and page 16 reference list checked. [2] is Balarin and Sangiovanni-Vincentelli. [15] is a personal communication from Lakhnech, which the sentence attributes to Balarin. Either the attribution or the reference number needs fixing, and only the authors know which was intended.
Second check: another model agreed
Report a problem with this finding
12 minor (typos and the like; most checked by the judge only)
Wording Introduction: "we identify the shortest prefix of the abstract counterexample that does not correspond to an actual trace ... The last abstract state in this prefix is split", but Section 4.3 partitions h^-1(ŝ_i), the state before the last state ŝ_{i+1} of that prefix.
- p. 2 Introduction, para 3
The last abstract state in this prefix is split into less abstract states
- p. 11 Section 4.3
We partition
Only the authors can say what is right here.
Judge's note: Page 2 (intro) and page 11 (Section 4.3) checked. In Section 4.3, S_i is non-empty and Img(S_i,R) ∩ h^-1(ŝ_{i+1}) = ∅, so the shortest non-corresponding prefix ends at ŝ_{i+1}. Yet h^-1(ŝ_i) is the state partitioned into S_{i,0}, S_{i,1} and S_{i,x}. In the Fig. 3 example, S4 is empty and ŝ3 is split. The overview wording does not match the algorithm. It would read correctly only if 'prefix' meant the longest prefix that does correspond.
Second check: another model agreed
Report a problem with this finding
Wording Conclusion refers to "the NP-complete separation problem" (p. 15), but Theorem 3 (p. 11) and the Introduction (p. 2) only state that "finding the coarsest refinement is NP-hard".
- p. 15 Section 7
the NP-complete separation problem
- p. 11 Theorem 3
The problem of finding the coarsest refinement is NP-hard
- p. 2 Introduction
finding the coarsest refinement is NP-hard
- p. 15 Section 7
NP-complete separation problem
Judge's note: Checked p. 11 (Theorem 3(i): 'NP-hard'; proof omitted, reduction from PARTITION INTO CLIQUES), the Introduction (text line 102: 'NP-hard') and p. 15 Section 7 ('NP-complete'). The paper never defines a decision version of the problem or argues that it is in NP. A decision version may well be in NP, so this is a wording inconsistency, not a false claim.
Second check: another model agreed
Report a problem with this finding
Wording Example 3: "Notice that S4 and therefore Img(S3, R) are both empty" infers in the wrong direction; S4 = Img(S3,R) ∩ h^-1(4̂), so emptiness of Img(S3,R) implies emptiness of S4, not conversely.
- p. 9 Example 3
Notice that S4 and therefore Img(S3, R) are both empty.
Only the authors can say what is right here.
Judge's note: Page 9 checked. By definition S_i := Img(S_{i-1},R) ∩ h^-1(ŝ_i), so an empty S4 does not imply an empty Img(S3,R). For example, a transition 9→7 would give Img = {7} while S4 stays empty. In Fig. 3, state 9 draws no outgoing arrow, so both sets really are empty and the conclusion stands. Only the stated inference is reversed.
Second check: another model agreed
Report a problem with this finding
Wording "it requires one magnitude less memory during model checking" is stated generally, but the table's |MC| column shows an order-of-magnitude reduction only for waterpress (129595 vs 3335); the other designs show 1.0–2.9×.
- p. 14 Section 6, text after table
it requires one magnitude
- p. 15 Section 6, top
less memory during model checking
- p. 14 Results table, |MC| columns
1155
- p. 14 Results table, |MC| columns
129595
Only the authors can say what is right here.
Judge's note: I read the p14 table from the image. |MC| COI vs ABS: gigamax 1822 vs 816, guidance 30467 vs 10670, p-queue 1155 vs 1114, waterpress 129595 vs 3335, PCI bus 926443 vs 350226. The sentence continues on p15. As worded, it overstates the general effect. The phrase is also missing 'order of'.
Second check: another model agreed
Report a problem with this finding
Typo Body text spells "Lind-Nielson and An-dersen [17]" while reference 17 reads "J. Lind-Nielsen and H. R. Andersen".
- p. 3 Introduction, related work
Lind-Nielson and An-dersen [17]
- p. 16 Reference 17
J. Lind-Nielsen and H. R. Andersen.
- p. 16 Reference 17
J. Lind-Nielsen and H. R. Andersen
- p. 3 Introduction
Lind-Nielson and An-
Judge's note: The page 3 image shows 'Lind-Nielson'. The page 16 reference list shows 'Lind-Nielsen'. This is a spelling inconsistency.
Second check: none (judge only)
Report a problem with this finding
Typo Missing full stop: "A more detailed comparison with related work will be given in the full version" ends without a period before "Summarizing, ...".
- p. 3 Introduction, end of related-work paragraph
with related work will be given in the full version
Judge's note: The page 3 image confirms there is no period after 'full version'.
Second check: none (judge only)
Report a problem with this finding
Typo Product of domains is typeset without the last ×: "D_{v1} × · · · D_{vn}" (p4) and "D1 × · · · Dn" (p6); the same pattern appears for the hatted D and D_{VC} on p6, while p6 also has the correct "D = D1 × · · · × Dn".
- p. 4 Section 2, first paragraph
D_{v1} × · · · D_{vn}
- p. 6 Paragraph after Fig. 2
D1 × · · · Dn
Judge's note: Page 4 (Section 2, first paragraph) and page 6 (paragraph after Fig. 2) checked. The final × before the last factor is missing in several places, although one formula on p6 includes it. This is cosmetic.
Second check: none (judge only)
Report a problem with this finding
Typo Misspelling: "the previously known poblem PARTITION INTO CLIQUES" should read "problem".
- p. 11 After Theorem 3
previously known poblem PARTITION INTO CLIQUES
- p. 11
previously known poblem PARTITION INTO CLIQUES can
Judge's note: The page 11 image shows 'poblem' in the paragraph after Theorem 3.
Second check: none (judge only)
Report a problem with this finding
Typo "use the algorithm Polyrefine to find the coarsest refinement" spells the algorithm differently from "PolyRefine" used elsewhere (Fig. 7, p11, p13).
- p. 12 Heuristics paragraph after Fig. 7
use the algorithm Polyrefine to find the coarsest refinement
Judge's note: The page 12 image shows 'Polyrefine' in the heuristics paragraph. The next sentence and the Fig. 7 caption use 'PolyRefine'. The difference is cosmetic.
Second check: none (judge only)
Report a problem with this finding
Typo Fujitsu processor is introduced as "multimedia assist (MMA-ASIC) processor" and then called "The RTL implementation of MM-ASIC" two sentences later (p. 15).
- p. 15 Section 6, Fujitsu paragraph
multimedia assist (MMA-ASIC) processor
- p. 15 Section 6, Fujitsu paragraph
mentation of MM-ASIC is described
- p. 15 Fujitsu paragraph
implementation of MM-ASIC
- p. 15 same paragraph
RTL implementation of MM-ASIC
Judge's note: In the page 15 image, the Fujitsu paragraph of Section 6 shows both 'MMA-ASIC' and 'MM-ASIC', and both refer to the same design. The second form is not defined anywhere, so the abbreviation is inconsistent. This is cosmetic.
Second check: none (judge only)
Report a problem with this finding
Typo Reference 10 gives the journal as "ACM Transactions on Programming Languages and System (TOPLAS)" (singular 'System').
- p. 16 Reference 10
Programming Languages and System (TOPLAS)
Only the authors can say what is right here.
Judge's note: Rests on outside knowledge: the journal's title is ACM Transactions on Programming Languages and Systems (plural). The page 16 image confirms that the reference reads 'Programming Languages and System (TOPLAS)'.
Second check: none (judge only)
Report a problem with this finding
Typo Reference 8 gives the publisher of Clarke, Grumberg and Peled's book as "Model Checking. MIT Publishers, 1999."
- p. 16 Reference 8
MIT Publishers, 1999.
- p. 16 Reference 8
Model Checking. MIT Publishers, 1999.
Only the authors can say what is right here.
Judge's note: Rests on outside knowledge: the book Model Checking (1999) was published by MIT Press. The page 16 image confirms that the reference reads 'MIT Publishers, 1999.'
Second check: none (judge only)