52:
concludes that the counterexample is attributed to inadequate precision of the abstraction. Otherwise, the process finds a bug in the program. Refinement is performed when a counterexample is found to be spurious. The iterative procedure terminates either if a bug is found or when the abstraction has been refined to the extent that it is equivalent to the original model.
535:
When counterexamples are found, they are examined to determine if they are spurious examples, i.e., they are unauthentic ones that emerge from the under-abstraction of the model. A non-spurious counterexample reflects the incorrectness of the program, which may be sufficient to terminate the program
51:
If a desired property for a program is not satisfied in the abstract model, a counterexample is generated. The CEGAR process then checks whether the counterexample is spurious, i.e., if the counterexample also applies to the under-abstraction but not the actual program. If this is the case, it
539:
The refinement process ensures that the dead-end states and the bad states do not belong to the same abstract state. A dead-end state is a reachable one with no outgoing transition whereas a bad-state is one with transitions causing the counterexample.
376:
677:. Automated Reasoning with Analytic Tableaux and Related Methods: 30th International Conference, TABLEAUX 2021, Birmingham, UK. Lecture Notes in Computer Science. Vol. 12842. Cham: Springer. pp. 74–91.
536:
verification process and conclude that the program is incorrect. The main objective of the refinement process handle spurious counterexamples. It eliminates them by increasing the granularity of the abstraction.
639:. International Conference on Computer Aided Verification CAV 2000: Computer Aided Verification. Lecture Notes in Computer Science. Vol. 1855. Berlin, Heidelberg: Springer. pp. 154–169.
159:
40:. Models for even small programs, however, may have an enormous number of states. This is identified as the state explosion problem. CEGAR addresses this problem with two stages —
505:
443:
396:
473:
211:
416:
299:
275:
253:
231:
182:
108:
556:, where a Kripke frame resembles the structure of state transition systems concerned in program verification, the CEGAR technique is also implemented for
304:
712:. Advanced Course on Petri Nets, ACPN 1996. Lecture Notes in Computer Science. Vol. 1491. Berlin, Heidelberg: Springer. pp. 429–528.
828:
775:
725:
690:
652:
519:
is performed for the abstract model. Bounded model checking, for instance, generates a propositional formula that is then checked for
507:
in the abstract model. The abstraction mapping also guarantees that the transition relations between two states are preserved.
762:. LASER Summer School on Software Engineering: LASER 2011. Lecture Notes in Computer Science. Vol. 7682. pp. 1–30.
72:
448:
To preserve the critical properties of the model, the abstraction mapping maps the initial state in the original model
30:
557:
113:
888:
37:
883:
23:
84:
520:
893:
478:
71:
To reason about the correctness of a program, particularly those involving the concept of time for
421:
79:
in automatic verification. The concept of abstraction is thus founded upon a mapping between two
806:
757:
672:
36:
In computer-aided verification and analysis of programs, models of computation often consist of
824:
771:
721:
686:
648:
75:, state transition models are used. In particular, finite-state models can be used along with
707:
381:
48:, which increases the precision of the abstraction to better approximate the original model.
857:
814:
802:
798:
763:
753:
713:
678:
640:
622:
601:
577:
553:
80:
66:
451:
189:
277:
is a function that labels each state with a set of propositional names that hold therein.
634:
516:
401:
284:
260:
238:
216:
167:
93:
76:
877:
626:
581:
630:
585:
371:{\displaystyle \langle S_{\alpha },s_{0}^{\alpha },R_{\alpha },L_{\alpha }\rangle }
819:
767:
717:
682:
549:
27:
862:
845:
674:
CEGAR-Tableaux: Improved Modal
Satisfiability via Modal Clause-Learning and SAT
589:
524:
605:
590:"Counterexample-guided abstraction refinement for symbolic model checking"
807:"Using Temporal Logic for Automatic Verification of Finite State Systems"
644:
756:; Klieber, William; Nováček, Miloš; Zuliani, Paolo (2011).
16:
A technique for symbolic model checking and logic calculi
813:. NATO ASI. Vol. 13. Berlin, Heidelberg: Springer.
846:"Efficient Strategies for CEGAR-Based Model Checking"
481:
454:
424:
404:
384:
307:
287:
263:
241:
219:
192:
170:
116:
96:
398:is an abstraction mapping that maps every state in
44:, which simplifies a model by grouping states, and
671:Goré, Rajeev; Kikkert, Cormac (6 September 2021).
499:
467:
437:
410:
390:
370:
293:
269:
247:
225:
205:
176:
153:
102:
844:Hajdu, Ákos; Micskei, Zoltán (11 November 2019).
748:
746:
744:
666:
664:
83:. Specifically, programs can be described with
759:Model Checking and the State Explosion Problem
8:
636:Counterexample-Guided Abstraction Refinement
365:
308:
148:
117:
20:Counterexample-guided abstraction refinement
617:
615:
154:{\displaystyle \langle S,s_{0},R,L\rangle }
861:
818:
491:
486:
480:
459:
453:
429:
423:
403:
383:
359:
346:
333:
328:
315:
306:
286:
262:
240:
218:
197:
191:
169:
130:
115:
95:
33:algorithms to optimise their efficiency.
811:Logics and Models of Concurrent Systems
569:
7:
255:is a total transition relation, and
14:
856:(4). Springer Nature: 1051–1091.
500:{\displaystyle s_{0}^{\alpha }}
850:Journal of Automated Reasoning
1:
820:10.1007/978-3-642-82453-1_1
768:10.1007/978-3-642-35746-6_1
718:10.1007/978-3-642-35746-6_1
709:The State Explosion Problem
683:10.1007/978-3-030-86059-2_5
438:{\displaystyle S_{\alpha }}
22:(CEGAR) is a technique for
910:
863:10.1007/s10817-019-09535-x
629:; Jha, Shomesh; Lu, Yuan;
584:; Jha, Shomesh; Lu, Yuan;
552:is often interpreted with
184:is a finite set of states,
90:Define a Kripke structure
64:
558:automated theorem proving
26:. It is also applied in
706:Valmari, Antti (1998).
391:{\displaystyle \alpha }
213:is an initial state in
24:symbolic model checking
801:; Browne, Michael C.;
521:Boolean satisfiability
501:
469:
439:
412:
392:
372:
295:
271:
249:
227:
207:
178:
155:
104:
606:10.1145/876638.876643
502:
470:
468:{\displaystyle s_{0}}
440:
413:
393:
373:
296:
272:
250:
228:
208:
206:{\displaystyle s_{0}}
179:
156:
105:
85:control flow automata
588:(1 September 2003).
479:
452:
422:
402:
382:
305:
285:
261:
239:
217:
190:
168:
114:
94:
56:Program verification
645:10.1007/10722167_15
515:In each iteration,
496:
475:to its counterpart
338:
594:Journal of the ACM
497:
482:
465:
435:
408:
388:
368:
324:
291:
281:An abstraction of
267:
245:
223:
203:
174:
151:
100:
830:978-3-642-82453-1
803:Emerson, E. Allen
777:978-3-642-35746-6
727:978-3-540-49442-3
692:978-3-030-86059-2
654:978-3-540-45047-4
411:{\displaystyle S}
294:{\displaystyle M}
270:{\displaystyle L}
248:{\displaystyle R}
226:{\displaystyle S}
177:{\displaystyle S}
103:{\displaystyle M}
81:Kripke structures
901:
868:
867:
865:
841:
835:
834:
822:
795:
789:
788:
786:
784:
750:
739:
738:
736:
734:
703:
697:
696:
668:
659:
658:
619:
610:
609:
574:
554:Kripke semantics
506:
504:
503:
498:
495:
490:
474:
472:
471:
466:
464:
463:
444:
442:
441:
436:
434:
433:
417:
415:
414:
409:
397:
395:
394:
389:
377:
375:
374:
369:
364:
363:
351:
350:
337:
332:
320:
319:
300:
298:
297:
292:
276:
274:
273:
268:
254:
252:
251:
246:
232:
230:
229:
224:
212:
210:
209:
204:
202:
201:
183:
181:
180:
175:
160:
158:
157:
152:
135:
134:
109:
107:
106:
101:
67:Kripke structure
909:
908:
904:
903:
902:
900:
899:
898:
889:Logical calculi
874:
873:
872:
871:
843:
842:
838:
831:
805:; Sistla, A.P.
797:
796:
792:
782:
780:
778:
752:
751:
742:
732:
730:
728:
705:
704:
700:
693:
670:
669:
662:
655:
621:
620:
613:
576:
575:
571:
566:
546:
544:Tableau calculi
533:
513:
477:
476:
455:
450:
449:
425:
420:
419:
400:
399:
380:
379:
355:
342:
311:
303:
302:
283:
282:
259:
258:
237:
236:
215:
214:
193:
188:
187:
166:
165:
126:
112:
111:
92:
91:
69:
63:
58:
31:tableau calculi
17:
12:
11:
5:
907:
905:
897:
896:
891:
886:
884:Model checking
876:
875:
870:
869:
836:
829:
799:Clarke, Edmund
790:
776:
754:Clarke, Edmund
740:
726:
698:
691:
660:
653:
627:Grumberg, Orna
623:Clarke, Edmund
611:
600:(5): 752–794.
582:Grumberg, Orna
578:Clarke, Edmund
568:
567:
565:
562:
545:
542:
532:
529:
517:model checking
512:
511:Model Checking
509:
494:
489:
485:
462:
458:
432:
428:
418:to a state in
407:
387:
367:
362:
358:
354:
349:
345:
341:
336:
331:
327:
323:
318:
314:
310:
301:is defined by
290:
279:
278:
266:
256:
244:
234:
222:
200:
196:
185:
173:
150:
147:
144:
141:
138:
133:
129:
125:
122:
119:
99:
77:temporal logic
62:
59:
57:
54:
15:
13:
10:
9:
6:
4:
3:
2:
906:
895:
892:
890:
887:
885:
882:
881:
879:
864:
859:
855:
851:
847:
840:
837:
832:
826:
821:
816:
812:
808:
804:
800:
794:
791:
779:
773:
769:
765:
761:
760:
755:
749:
747:
745:
741:
729:
723:
719:
715:
711:
710:
702:
699:
694:
688:
684:
680:
676:
675:
667:
665:
661:
656:
650:
646:
642:
638:
637:
632:
631:Veith, Helmut
628:
624:
618:
616:
612:
607:
603:
599:
595:
591:
587:
586:Veith, Helmut
583:
579:
573:
570:
563:
561:
559:
555:
551:
543:
541:
537:
530:
528:
526:
522:
518:
510:
508:
492:
487:
483:
460:
456:
446:
430:
426:
405:
385:
360:
356:
352:
347:
343:
339:
334:
329:
325:
321:
316:
312:
288:
264:
257:
242:
235:
220:
198:
194:
186:
171:
164:
163:
162:
145:
142:
139:
136:
131:
127:
123:
120:
97:
88:
86:
82:
78:
74:
68:
60:
55:
53:
49:
47:
43:
39:
34:
32:
29:
25:
21:
853:
849:
839:
810:
793:
781:. Retrieved
758:
731:. Retrieved
708:
701:
673:
635:
597:
593:
572:
547:
538:
534:
514:
447:
280:
89:
70:
50:
45:
41:
35:
19:
18:
894:Modal logic
783:27 December
733:27 December
550:modal logic
73:concurrency
61:Abstraction
42:abstraction
28:modal logic
878:Categories
564:References
531:Refinement
525:SAT solver
65:See also:
46:refinement
493:α
431:α
386:α
366:⟩
361:α
348:α
335:α
317:α
309:⟨
149:⟩
118:⟨
633:(2000).
161:, where
87:(CFA).
827:
774:
724:
689:
651:
548:Since
378:where
38:states
523:by a
825:ISBN
785:2023
772:ISBN
735:2023
722:ISBN
687:ISBN
649:ISBN
858:doi
815:doi
764:doi
714:doi
679:doi
641:doi
602:doi
110:as
880::
854:64
852:.
848:.
823:.
809:.
770:.
743:^
720:.
685:.
663:^
647:.
625:;
614:^
598:50
596:.
592:.
580:;
560:.
527:.
445:.
866:.
860::
833:.
817::
787:.
766::
737:.
716::
695:.
681::
657:.
643::
608:.
604::
488:0
484:s
461:0
457:s
427:S
406:S
357:L
353:,
344:R
340:,
330:0
326:s
322:,
313:S
289:M
265:L
243:R
233:,
221:S
199:0
195:s
172:S
146:L
143:,
140:R
137:,
132:0
128:s
124:,
121:S
98:M
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.