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 and
               Andr{\'e} 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 and 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
    \url{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.}
}```