Christian Jacobi

Education and Research and Development Interests

• I studied Computer Science at Saarland University, Germany. I received a degree as "Diplom Informatiker" (Master Computer Science) in 1999.
• From 1999 to 2002, I was affiliated with Saarland University, Institute for Computer Architecture, as a Research Assistant; in 2002 I finished my doctoral thesis "Formal Verification of a Fully IEEE Compliant Floating Point Unit" and received a doctoral degree in computer science.
• My current interests are microprocessor design and (formal) verification, in particular in the area of memory caches; previously I have worked on floating point units, automatic formal verification, theorem proving, and logic and physical design.

Thesis

• Master thesis: Ein relationales Datenbanksystem für die SB-PRAM; Concurrency Control und der TPC-B-Benchmark (in German; A relational database system for the SB-PRAM; concurrency control and the TPC-B Benchmark)
  (pdf) (bibtex)
• Doctoral thesis: Formal Verification of a Fully IEEE Compliant Floating Point Unit
  (abstract) (pdf) (bibtex)

Publications

Journal Papers

• Formal Verification of the VAMP Floating Point Unit
  Christian Jacobi, Christoph Berg
  Formal Methods in System Design, Vol 26:3, pg 227-266, Springer, 2005
  (abstract) (pdf) (bibtex)
  
  
• Putting it all together – Formal verification of the VAMP
  Sven Beyer, Christian Jacobi, Daniel Kröning, Dirk Leinenbach, Wolfgang J. Paul
  International Journal on Software Tools for Technology Transfer (STTT), Vol 8:4-5, Springer, 2006
  (abstract) (pdf)
  
  
• A fully pipelined single-precision floating-point unit in the synergistic processor element of a CELL processor
  Hwa-Joon Oh, Silvia M. Mueller, Christian Jacobi, Kevin D. Tran, Scott R. Cottier, Brad W. Michael, Hiroo Nishikawa, Yonetaro Totsuka, Tatsuya Namatame, Naoka Yano, Takashi Machida, Sang H. Dhong
  IEEE Journal of Solid-State Circuits, Vol. 41:4, pg 759-771, IEEE, 2006
  (abstract) (pdf)
  
  
• IBM POWER6 accelerators: VMX and DFU
  Lee Eisen, J. J. Wes Ward III, Hans-Werner Tast, Nicolas Mäding, Jens Leenstra, Silvia M. Mueller, Christian Jacobi, Jochen Preiss, Eric M. Schwarz, Steven R. Carlough
  IBM Journal of Research and Development, Vol. 51:6, IBM, 2007
  (abstract) (pdf)
  
  

Conference Papers

• Highly concurrent locking in shared memory database systems
  Christian Jacobi, Cédric Lichtenau
  Proceedings of EUROPAR '99, Springer LNCS 1685, pg 477, 1999
  (abstract) (pdf) (bibtex)
  
  
• Proving the Correctness of a Complete Microprocessor
  Christian Jacobi, Daniel Kröning
  Informatik 2000, 30. Jahrestagung der Gesellschaft für Informatik, Springer-Verlag Informatik aktuell, 2000
  (abstract) (pdf) (bibtex)
  
  
• Formal Verification of a Basic Circuits Library
  Christoph Berg, Christian Jacobi, Daniel Kröning
  Proceedings of the IASTED International Conference on Applied Informatics, Innsbruck (AI 2001), ACTA Press, 2001
  (abstract) (pdf) (bibtex)
  
  
• Formal Verification of the VAMP Floating Point Unit
  Christoph Berg, Christian Jacobi
  Proceedings of 11th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME), Springer LNCS 2144, pg 325, 2001
  (abstract) (pdf) (bibtex)
  
  
• Formal Verification of Complex Out-of-order Pipelines by Combining Model-Checking and Theorem-Proving
  Christian Jacobi
  Proceedings of Computer Aided Verification, 14th International Conference (CAV 2002), Springer LNCS 2404, pg 309, 2002
  (abstract) (pdf) (bibtex)
  
  
• Deriving Cryptographically Sound Implementations Using Composition and Formally Verified Bisimulation
  Michael Backes, Christian Jacobi, Birgit Pfitzmann
  Proceedings of FME 2002: Formal Methods - Getting IT Right, International Symposium of Formal Methods Europe (FME 2002), Springer LNCS 2391, pg 310, 2002
  (abstract) (pdf) (bibtex)
  
  
• Cryptographically Sound and Machine-Assisted Verification of Security Protocols
  Michael Backes, Christian Jacobi
  Proceedings of STACS 2003, 20th Annual Symposium on Theoretical Aspects of Computer Science, Springer LNCS 2607, pg 675, 2003
  (abstract) (pdf) (bibtex)
  
  
• Instantiating Uninterpreted Functional Units and Memory System: Functional Verification of the VAMP Processor
  Sven Beyer, Christian Jacobi, Daniel Kröning, Dirk Leinenbach, Wolfgang J. Paul
  Proceedings of 12th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME), Springer LNCS 2860, pg 51, 2003
  (abstract) (pdf) (bibtex)
  
  
• Efficient Symbolic Simulation via Dynamic Scheduling, Don’t Caring, and Case Splitting
  Viresh Paruthi, Christian Jacobi, Kai Weber
  Proceedings of 13th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME), Springer LNCS 3725, pg 114, 2005
  (abstract) (pdf)
  
  
• Automatic Formal Verification of Fused-Multiply-Add FPUs
  Christian Jacobi, Kai Weber, Viresh Paruthi, Jason Baumgartner
  Proceedings of Design, Automation and Test in Europe (DATE'05), IEEE, 2005
  (abstract) (pdf)
  
  
• The vector floating-point unit in a synergistic processor element of a CELL processor Silvia Mueller, Christian Jacobi, Hwa-Joon Oh, Kevin D. Tran, Scott R. Cottier, Brad W. Michael, Hiroo Nishikawa, Yonetaro Totsuka, Tatsuya Namatame, Naoka Yano, Takashi Machida, Sang H. Dhong
  Proceedings of the 17th IEEE Symposium on Computer Arithmetic (ARITH 05), IEEE, 2005
  (abstract) (pdf)
  
  
• A fully-pipelined single-precision floating point unit in the synergistic processor element of a CELL processor
  Hwa-Joon Oh, Silvia M. Mueller, Christian Jacobi, Kevin D. Tran, Scott R. Cottier, Brad W. Michael, Hiroo Nishikawa, Yonetaro Totsuka, Tatsuya Namatame, Naoka Yano, Takashi Machida, Sang H. Dhong
  IEEE Symposium on VLSI Circuits (VLSI'05), IEEE, 2005
  (abstract) (pdf)
  
  
• Evaluating Coverage of Error Detection Logic for Soft Errors using Formal Methods
  Udo Krautz, Matthias Pflanz, Christian Jacobi, Hans-Werner Tast, Kai Weber, Heinrich T. Vierhaus
  Proceedings of Design, Automation and Test in Europe (DATE'06), IEEE, 2006
  (abstract) (pdf)
  
  
• Verifying full-custom multipliers by Boolean equivalence checking and an arithmetic bit level proof
  Udo Krautz, Markus Wedler, Wolfgang Kunz, Kai Weber, Christian Jacobi, Matthias Pflanz
  Proceedings of Asia and South Pacific Design Automation Conference (ASPDAC 2008), IEEE, 2008
  (abstract) (pdf)
  
  

Invited Talks

• Formal Verification in Industry -- Current State and Future Directions
  Presented at FMCAD Workshop 2006, San Jose, CA.
  (Powerpoint)
  
  

Workshop Papers / Posters / Technical Reports

• Formal Verification of a Theory of IEEE Rounding
  Christian Jacobi
  Theorem Proving in Higher-Order Logics (TPHOLs) 2001: Supplemental Proceedings; Informatics Research Report EDI-INF-RR-0046, Univ. Edinburgh, UK, 2001
  (abstract) (pdf) (bibtex)
  
  
• Formal Verification of the VAMP processor (Project Status)
  Christoph Berg, Sven Beyer, Christian Jacobi, Daniel Kröning, Dirk Leinenbach
  Symposium on the Effectiveness of Logic in Computer Science (ELICS02), Technical Report MPI-I-2002-2-007, Max-Planck-Institut für Informatik, Saarbruecken, Germany, 2002
  (abstract) (pdf) (bibtex)