|
|
|
I work on the design and verification of a new specialized supercomputer for protein simulations.
Email: 
Course announcement for Columbia University students:
Formal Verification of Hardware and Software Systems
The course homepage is at https://sites.google.com/site/csee6863/
Publications:
- 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)
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
Education:
Postdoctoral Fellow in Computer Science at CMU (Host: Ed Clarke), 2002-2004
Ph.D. in Computer Science,
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)