Navigation

Contact

  • E-Mail: stzv4/kephvksanie/a15.kemrksper@isjcjnformatu4ikk5qx7.uni-xhznuolvzkc7dedginburg.de

Curriculum Vitae

10/1999 - 01/2006Studies of Computer Science at University of Oldenburg
01/2006Diploma degree (with distinction) in Computer Science at University of Oldenburg
02/2006 - 03/2011Research Assistant at Centrum Wiskunde & Informatica, Amsterdam, The Netherlands (www.cwi.nl)
12/2011PhD defense at the university of Leiden (NL), dissertation title "Modelling and Analysis of Real-Time Coordination Patterns"
04/2011 - 06/2012Research Assistant in the Correct System Design Group
07/2012 - 04/2015Research Assistant at OFFIS, Group SAV-RSM
since 04/2015Research Assistant in the Correct System Design Group

Research

My research interests are

  • Real-time Systems (Timed Automata, Timed Constraint Automata, ...)
  • Verification and model checking
  • SAT-based model checking
  • Automata theory
  • (Coordination in) Component-based systems 

Publications

  • [inproceedings] bibtex | Go to document Go to document
    S. Kemper and C. Etzien, "A Visual Logic for the Description of Highway Traffic Scenarios," in Proc. Complex Systems Design & Management, Proceedings of the Fourth International Conference on Complex Systems Design & Management CSD&M 2013, Paris, France, December 4-6, 2013, 2013, pp. 233-245.
    @inproceedings{DBLP:conf/csdm/KemperE13,
      author = {Stephanie Kemper and Christoph Etzien},
      title = {A Visual Logic for the Description of Highway Traffic Scenarios},
      booktitle = {Complex Systems Design {\&} Management, Proceedings of the Fourth International Conference on Complex Systems Design {\&} Management CSD{\&}M 2013, Paris, France, December 4-6, 2013},
      pages = {233--245},
      year = {2013},
      url = {http://dx.doi.org/10.1007/978-3-319-02812-5_17},
      doi = {10.1007/978-3-319-02812-5_17},
      timestamp = {Sun, 08 Dec 2013 13:34:23 +0100},
      biburl = {http://dblp.uni-trier.de/rec/bib/conf/csdm/KemperE13},
      bibsource = {dblp computer science bibliography, http://dblp.org} }
  • S. Kemper, "SAT-based verification for timed component connectors," Science of Computer Programming, vol. 77, iss. 7–8, pp. 779-798, 2012.
    @article{Kemper2012779,
      author = {S. Kemper},
      title = {SAT-based verification for timed component connectors },
      journal = {Science of Computer Programming },
      year = {2012},
      volume = {77},
      pages = {779 - 798},
      number = {7–8},
      note = {(1) FOCLASA’09 (2) FSEN’09 },
      abstract = {Component-based software construction relies on suitable models underlying components, and in particular the coordinators which orchestrate component behaviour. Verifying correctness and safety of such systems amounts to model checking the underlying system model. The model checking techniques not only need to be correct (since system sizes increase), but also scalable and efficient. In this paper, we present a SAT-based approach for bounded model checking of Timed Constraint Automata, which permits true concurrency in the timed orchestration of components. We present an embedding of bounded model checking into propositional logic with linear arithmetic. We define a product that is linear in the size of the system, and in this way overcome the state explosion problem to deal with larger systems. To further improve model checking performance, we show how to embed our approach into an extension of counterexample guided abstraction refinement with Craig interpolants. },
      doi = {http://dx.doi.org/10.1016/j.scico.2011.02.003},
      issn = {0167-6423},
      keywords = {Timed constraint automata},
      url = {http://www.sciencedirect.com/science/article/pii/S0167642311000499} }
  • [inproceedings] bibtex | Go to document Go to document
    S. Kemper, "Compositional Construction of Real-Time Dataflow Networks," in Proc. Coordination Models and Languages, 12th International Conference, COORDINATION 2010, Amsterdam, The Netherlands, June 7-9, 2010. Proceedings, 2010, pp. 92-106.
    @inproceedings{Kem10,
      author = {Stephanie Kemper},
      editor = {Dave Clarke and Gul A. Agha},
      title = {Compositional Construction of Real-Time Dataflow Networks},
      booktitle = {Coordination Models and Languages, 12th International Conference, COORDINATION 2010, Amsterdam, The Netherlands, June 7-9, 2010. Proceedings},
      publisher = {Springer},
      series = {Lecture Notes in Computer Science},
      volume = {6116},
      year = {2010},
      pages = {92-106},
      doi = {10.1007/978-3-642-13414-2_7},
      url = {http://csd.informatik.uni-oldenburg.de/~stephie/Kemper_COORDINATION10.pdf} }
  • S. Kemper, "SAT-based Verification for Timed Component Connectors," Electr. Notes Theor. Comput. Sci., vol. 255, pp. 103-118, 2009.
    @article{Kem09,
      author = {Stephanie Kemper},
      title = {{SAT}-based {V}erification for {T}imed {C}omponent {C}onnectors},
      journal = {Electr. Notes Theor. Comput. Sci.},
      volume = {255},
      year = {2009},
      pages = {103-118},
      url = {http://csd.informatik.uni-oldenburg.de/~stephie/Kemper_FOCLASA09.pdf},
      doi = {10.1016/j.entcs.2009.10.027},
      keywords = {Timed Constraint Automata, Abstraction Refinement, Model Checking, SAT, Component-Based Software Engineering} }
  • [inproceedings] bibtex | Go to document Go to document
    S. Kemper and A. Platzer, "SAT-based Abstraction Refinement for Real-time Systems," in Proc. Formal Aspects of Component Software, Third International Workshop, FACS 2006, Prague, Czech Republic, Proceedings, 2007, pp. 107-122.
    @inproceedings{DBLP:journals/entcs/KemperP07,
      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},
      url = {http://symbolaris.com/pub/SAAtRe.pdf},
      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. With a faithful embedding of bounded model checking for systems of timed automata into propositional logic and linear arithmetic, we achieve both, quick abstraction techniques and a linear-size representation of parallel composition. In this logical setting, we introduce an abstraction 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. } }

Theses

  • [phdthesis] bibtex
    S. Kemper, "Modelling and Analysis of Real-Time Coordination Patterns," PhD Thesis , 2011.
    @PHDTHESIS{Kem11phd,
      author = {Stephanie Kemper},
      title = {Modelling and Analysis of Real-Time Coordination Patterns},
      school = {{Leiden Institute of Advanced Computer Science (LIACS)}},
      year = {2011},
      adress = {Leiden, The Netherlands},
      isbn = {978-90-8891-360-0},
      pages = {165} }
  • [mastersthesis] bibtex | Go to document Go to document
    S. Kemper, "SAT-based Verification for Abstraction Refinement," Master's Dissertation , 2006.
    @MASTERSTHESIS{Kem06,
      author = {Kemper, Stephanie},
      title = {{SAT}-based Verification for Abstraction Refinement},
      school = {University of Oldenburg},
      year = {2006},
      month = {January},
      url = {http://csd.informatik.uni-oldenburg.de/~skript/pub/diplom/kemper06.pdf} }
Webmasvstejpcjr (m.gogoslie6kpuyseking@b7uol.deyqmnt) (Changed: 2020-01-23)