Michael Theobald

D. E.  Shaw Research

I work on the design and verification of a new specialized supercomputer for protein simulations.


Course announcement for Columbia University students:

              Formal Verification of Hardware and Software Systems

               The course homepage is at https://sites.google.com/site/csee6863/





  •                    Proof-Guided Underapproximation-Widening for Multi-Process Systems (POPL 2005)
  •              Generalized Latency-Insensitive Systems for Single-Clock and Multi-Clock Architectures (DATE 2004)
  •              SAT-Based Algorithms for Logic Minimization (ICCD 2003)
  •              Symbolic Model Checking of Software (SoftMC 2003)
  •              Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems (IJFCS 2003)
  •              Generalized Latency-Insensitive Systems for GALS Architectures (FMGALS 2003)
  •              Verification of Hybrid Systems Based on Counterexample-Guided Abstraction Refinement (TACAS 2003)
  •              Efficient Algorithms for the Design of Asynchronous Control Circuits (Ph.D. thesis, 2002)

All Publications

Research Interests:


  • Asynchronous (“clock-less”) Circuits
  • Formal Verification of Software and Hardware
  • Computer-Aided Design (CAD), Logic and High-Level Synthesis, BDD and SAT Techniques
  • Efficient Algorithms and Data Structures, Combinatorial Optimization
  • Formal Methods
  • Embedded and Hybrid Systems
  • Practical Applications in Systems Biology, Medical Devices, Robotics



Postdoctoral Fellow in Computer Science at CMU (Host: Ed Clarke), 2002-2004

Ph.D. in Computer Science, Columbia University, New York, 2002.

Thesis: Efficient Algorithms for the Design of Asynchronous Control Circuits (Advisor: Steven Nowick)


Diplom in Computer Science, Johann Wolfgang Goethe-Universitaet, Frankfurt/Main, 1994.
Thesis: Ordered Kronecker Functional Decision Diagrams (Advisor: Bernd Becker)