Contact

Dipl.-Inf. Stefan Disch

Chair of Operating Systems

Institute of Computer Science
Albert-Ludwigs-Universität
Georges Köhler Allee 51, Room 02..031
79110 Freiburg im Breisgau
Germany

Phone +49 (0)761 203 8187
Fax +49 (0)761 203 8142

Email: disch@informatik.uni-freiburg.de

Research

• Research Interests
  • AND-Inverter-Graphs
  • Data structures for Model-Checking of hybrid systems
  • SAT- and QSAT-solvers and the application in formal verification
  • SMT-Solvers and their application in formal verification
• Projects
  • AVACS (Transregional Colloborative Research Center, funded by the DFG)
  • Automatisierte Verifikationstechniken bei unvollständiger Information (supported by the DFG)

Publications

• Christoph Scholl, Stefan Disch, Florian Pigorsch, and Stefan Kupferschmid
  Computing Optimized Representations for Non-convex Polyhedra by Detection and Removal of Redundant Linear Constraints
  Fifteenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)
  22 - 29 March, 2009, York, UK
  → SpringerLink
  
• Christoph Scholl, Stefan Disch, Florian Pigorsch, and Stefan Kupferschmid
  Using an SMT solver and Craig interpolation to detect and remove redundant linear constraints in representations of non-convex polyhedra
  6th International Workshop on Satisfiability Modulo Theories
  July 7-8, 2008, Princeton, USA
  → ACM
  
• Werner Damm, Stefan Disch, Hardi Hungar, Swen Jacobs, Jun Pang, Florian Pigorsch, Christoph Scholl, Uwe Waldmann, and Boris Wirtz
  Exact state set representation in the verification of linear hybrid systems with large discrete state space
  5th International Symposium on Automated Technology for Verification and Analysis (ATVA)
  October 22-25, 2007, Tokyo, Japan
  → PDF | → Slides (PDF) | → SpringerLink
  
• Werner Damm, Stefan Disch, Hardi Hungar, Swen Jacobs, Jun Pang, Florian Pigorsch, Christoph Scholl, Uwe Waldmann, and Boris Wirtz
  Exact state set representation in the verification of linear hybrid systems with large discrete state space
  AVACS Technical Report No. 21, SFB/TR 14 AVACS, June 2007. ISSN: 1860-9821
  → PDF | → Bibtex
• Stefan Disch, Christoph Scholl
  Combinational Equivalence Checking Using Incremental SAT Solving, Output Ordering, and Resets
  12th Asia and South Pacific Design Automation Conference (ASP-DAC)
  January 23-27 2007, Yokohama, Japan
  → PDF | → Bibtex | → Slides (PDF) | → IEEE Xplore Link
• Florian Pigorsch, Christoph Scholl, Stefan Disch
  Advanced Unbounded Model Checking Based on AIGs, BDD Sweeping, And Quantifier Scheduling
  Formal Methods in Computer Aided Design (FMCAD)
  November 12-16 2006, San Jose, CA, USA
  → PDF | → Bibtex | → IEEE Xplore Link
• Werner Damm, Stefan Disch, Hardi Hungar, Jun Pang, Florian Pigorsch, Christoph Scholl, Uwe Waldmann, Boris Wirtz
  Automatic Verification of Hybrid Systems with Large Discrete State Space
  4th International Symposium on Automated Technology for Verification and Analysis (ATVA)
  23-26 October 2006, Beijing, China
  → PDF | → Bibtex | → SpringerLink
• Florian Pigorsch, Christoph Scholl, Stefan Disch
  Advanced unbounded model checking by using AIGs, BDD sweeping and quantifier scheduling
  9th ITG/GI/GMM Workshop "Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen"
  February 2006, Dresden, Germany
  → PDF | → Bibtex
• Stefan Disch
  SAT basierte Black-Box Verifikation
  Diploma thesis, Albert-Ludwigs-University, Freiburg, July 2004.

Teaching support

• Summer term 2004:
  
  • Computer-Aided-Engineering (lab with the Mentor Graphics FPGA Advantage tool)
• Winter term 2004/2005:
  
  • Heuristiken zur Lösung von SAT- und QSAT-Problemen (seminar)
• Summer term 2005:
  
  • Computer-Aided-Engineering (lab using VIS and CUDD)
  • The SPIN model checker (seminar)
• Winter term 2005/2006
  
  • Systeme I (lecture)
• Summer term 2006
  
  • Verifikation und Fehlerdiagnose (seminar)
• Summer term 2007
  
  • Rechnerarchitektur (lecture)
• Winter term 2008/2009
  
  • Systeme I (lecture)
• Winter term 2009/2010
  
  • Embedded Systems I (lecture)
• Diploma thesis: SAT-basierte Lösung von Überdeckungsproblemen, 2008, Larissa Wißmann
• Studienarbeit: Visualisierung linearer And-Inverter-Graphen, 2007, Jan Markstahler
• Studienarbeit: Kombinatorische Äquivalenztests mittels inkrementeller SAT-Solver, Ausgangssortierheuristiken und Resetstrategien, 2007, Bernhard Zimmermann
• Bachelor thesis: Erstellung und Erprobung eines USB Profils für Sick Geräte mit der internen Kommunikationsschnittstelle NAPI, 2007, Nils Langner
• Diploma thesis: And-Inverter-Graphen und deren Anwendung in der Verifikation, 2005, Florian Pigorsch
• Studienarbeit: Vom Prozessor zur Lichtsteuerung, 2005, Dominik Alpers

Biography

• 1989-1992: Industrial education in the field of high precession optics (Feinoptik) at the Erwin Sick AG, Waldkirch, Germany
• 1992 - 1994: university-entrance diploma (Abitur), Technische Oberschule, Freiburg
• 1994 - 1996: Civilian service, Psychiatrisches Landeskrankenhaus Emmendingen
• 1996, May - September: Alpina, Waldkirch
• 1996 - 2004: Study of computer science (diploma) at the Albert-Ludwigs-Universität Freiburg and several jobs at the university (system administration (at the fdm) and teaching support)
• August 16th, 2004 - August 15th, 2006: PhD student at the chair of operating systems (Prof. Dr. Christoph Scholl) and chair of computer architecture (Prof. Bernd Becker)
  
• Since August 16th, 2006: PhD student at the chair of operating systems (Prof. Dr. Christoph Scholl)
  

Links

• University of Freiburg
• Chair of Computer Architecture
• Chair of Operating Systems
• AVACS
  Automatic Verification and Analysis of Complex Systems, project homepage
• BillardGL
  OpenGL based billard game, published under the GPL, written by Tobias Nopper, Martina Welte and me.