SAT-based abstraction refinement for real-time systems

@inproceedings{DBLP:journals/entcs/KemperP07,
	pdf = {pub/SAAtRe.pdf},
	slides = {pub/SAAtRe-slides.pdf},
	author = {['Stephanie Kemper', 'André Platzer']},
	title = {SAT-based Abstraction Refinement for
               Real-time Systems},
	booktitle = {Formal Aspects of Component Software, Third
               International Workshop, FACS 2006, Prague,
               Czech Republic, Proceedings},
	year = {2007},
	editor = {['Frank S. de Boer', 'Vladimir Mencl']},
	journal = {Electr. Notes Theor. Comput. Sci.},
	volume = {182},
	series = {ENTCS},
	issn = {1571-0661},
	pages = {107-122},
	doi = {10.1016/j.entcs.2006.09.034},
	annote = {Appeared as UNU-IIST Report No. 344
    http://www.iist.unu.edu/newrh/III/1/docs/techreports/report344.html},
	keywords = {abstraction refinement, model checking,
              real-time systems, SAT, Craig interpolation},
	abstract = {
   In this paper, we present an abstraction refinement
   approach for model checking safety properties of
   real-time systems using SAT-solving. We present a
   faithful embedding of bounded model checking for systems
   of timed automata into propositional logic with linear
   arithmetic and prove correctness. With this logical
   representation, we achieve a linear-size representation
   of parallel composition and introduce a quick
   abstraction technique that works uniformly for clocks,
   events, and states. When necessary, abstractions are
   refined by analysing spurious counterexamples using a
   promising extension of counterexample-guided abstraction
   refinement with syntactic information about Craig
   interpolants. To support generalisations, our overall
   approach identifies the algebraic and logical principles
   required for logic-based abstraction refinement.}
}