Silke Wagner

Office: Wean Hall 4106
Phone: +1 412-268-9331 (8-9331 on campus)
E-mail: silkwa@cs.cmu.edu

Research Interests

• Automatic verification of hybrid system stability


• Liveness verification of linear hybrid systems


• Liveness and safety verification of embedded systems

Education

January 2008 - :

Postdoctoral fellow at Carnegie Mellon University with Professor Edmund M. Clarke.

November 2003 - December 2007:

Ph.D. Student at the MPI.

October 1998 - September 2003:

Studies in Mathematics (major) and Computer Science (minor) at University of Saarbrücken (Universität des Saarlandes). Title of Diploma Thesis: Extrapolationsmethoden für die Wärmeleitungsgleichung (supervisor: Prof. Dr. Joachim Weickert).

August 1989 - June 1998:

High School: Marie-Luise Kaschnitz Gymnasium Vöklingen

Publications

• Control Software Model Checking Using Bisimulation Functions for Nonlinear Systems.
  In Conference on Decision and Control (CDC), Cancun, Mexico, December 2008 (to appear).


• Stability Proofs for Hybrid Systems.
  Ph.D. thesis, Universität des Saarlandes, 2007.


• Region Stability Proofs for Hybrid Systems.
  In Formal Modelling and Analysis of Timed Systems (FORMATS), Salzburg, Austria, October 2007.


• A Sound and Complete Proof Rule for Region Stability of Hybrid Systems.
  In Hybrid Systems: Computation and Control (HSCC), Pisa, Italy, April 2007.


• A Method and a Tool for Automatic Verification of Region Stability for Hybrid Systems.
  Technical report, in MPI-I-2007-2-001, January 2007.


• Model Checking of Hybrid Systems: From Reachability towards Stability.
  In Hybrid Systems: Computation and Control (HSCC), Santa Barbara (CA), USA, March 2006.


• Summaries for While Programs with Recursion.
  In European Symposium on Programming (ESOP), Edinburgh, Scotland, April 2005.


• Summaries for While Programs with Recursion.
  Technical report, in MPI-I-2004-2-007, December 2004.


• Extrapolationsmethoden für die Wärmeleitungsgleichung.
  Diploma thesis, July 2003.

Tools

AuVeRS: a model checker for automatic verification of region stability for hybrid systems.

LHAlive: a model checker for verification of liveness properties for linear hybrid automata.

Talks

• AVACS workshop, Freiburg, Feb. 2004: Stability of Hybrid Systems


• AVACS workshop, Oldenburg, March 2005: Model Checking for Stability Properties of Linear Hybrid Automata


• ESOP conference, Edinburgh, April 2005: Summaries for While Programs with Recursion


• AVACS workshop, Saarbrücken, March 2006


• HSCC conference, Santa Barbara, March 2006: Model Checking of Hybrid Systems: From Reachability towards Stability


• Seminar on Simulation and Verification of Dynamic Systems, Dagstuhl, April 2006


• Ringvorlesung der Informatik, Saarbrücken, Nov. 2006: Region Stability of Hybrid Systems


• AVACS workshop, Saarbrücken, March 2007


• SVC seminar, Pittsburgh, February 2008: Stability Proofs for Hybrid Systems

Summer Schools and Seminars

• 12 - 19 September 2004 : Summer School on Formal Methods for the Design of Computer, Communication and Software Systems: Real Time
  University Residential Centre in Bertinoro, Italy


• 10 - 17 July 2005 : Lipari School on Formal Methods: Theory And Practice
  Lipari Island, Italy


• 17 - 22 April 2006 : Dagstuhl-Seminar on Simulation and Verification of Dynamic Systems
  Schloss Dagstuhl, Germany