Selected publications by Stefan Schwoon

Abstract:
Counterexample-guided abstraction refinement (CEGAR) has proven to be a powerful method for software model-checking. In this paper, we investigate this concept in the context of sequential (possibly recursive) programs whose statements are given as BDDs. We examine how Craig interpolants can be computed efficiently in this case and propose a new, special type of interpolants. Moreover, we show how to treat multiple counterexamples in one refinement cycle. We have implemented this approach within the model-checker Moped and report on experiments.

@inproceedings{EKS-tacas06,
   address = {Vienna, Austria},
   author = {Javier Esparza and Stefan Kiefer and Stefan Schwoon},
   booktitle = {{P}roceedings of the 12th {I}nternational {C}onference on {T}ools and {A}lgorithms for {C}onstruction and {A}nalysis of {S}ystems ({TACAS}'06)},
   DOI = {10.1007/11691372_35},
   editor = {Hermanns, Holger and Palsberg, Jens},
   month = mar,
   pages = {489-503},
   publisher = {Springer},
   series = {Lecture Notes in Computer Science},
   title = {Abstraction Refinement with {C}raig Interpolation and Symbolic Pushdown Systems},
   url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EKS-tacas06.pdf},
   volume = {3920},
   year = {2006},
}

About LSV