Christoph Sprenger's Publications

Articles

• Simulation Logic, Applets and Compositional Verification, with Dilian Gurov and Marieke Huisman, submitted to POPL 04, July, 2002 (gzipped PostScript, Postscript), more detailed version available as INRIA Techreport No. 4890 (gzipped PostScript, Postscript)

 
• A verification methodology for infinite-state message passing systems, with K. Worytkiewicz, ACM & IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE'2003), Mont Saint-Michel, France, June 24-26, 2003 (gzipped PostScript, Postscript)

 
• On the structure of inductive reasoning: circular and tree-shaped proofs in the µ-calculus, with Mads Dam, Foundations of Software Science and Computation Structures, FOSSACS '03, Warsaw, Poland, LNCS 2620,  pp. 425-440, 2003 (gzipped PostScript, Postscript)

 
• A note on global induction mechanisms in a µ-calculus with explicit approximations, with Mads Dam, full version of FICS '02 paper, accepted for publication in Theoretical Informatics and Applications, July 2003 (gzipped Postscript, Postscript)

 
• A note on global induction mechanisms in a µ-calculus with explicit approximations, with Mads Dam, Fixed Points in Computer Science, FICS '02, Copenhagen, Denmark, July 20-21, 2002 (gzipped Postscript, Postscript)

 
• A verified model checker for the modal µ-calculus in Coq, In Tools and Algorithms for the Construction and Analysis of Systems, TACAS '98, Lisbon, Portugal, LNCS 1384, pp. 167-183, 1998 (gzipped Postscript, Postscript)

 
• Sciddle - A tool for large scale distributed computing, with P. Arbenz, H.P. Lüthi and S. Vogel, Concurrency: Practice and Experience, Vol. 7(2), pp. 121-146, April 1995

 
• A parallel implementation of the symmetric tridiagonal QR algorithm, co-author, with P. Arbenz and K. Gates, Proc. of the 14th Symposium on the Frontiers of Massively Parallel Computation, McLean, Virginia, October 19-21, 1992

 

Theses

• Deductive Local Model Checking - On the Verification of CTL* Properties of Infinite-State Reactive Systems, Ph.D. Thesis No. 2215, Swiss Federal Institute of Technology, Lausanne, Switzerland, 2000 (details here)

 
• Network Computing with Non-Blocking Remote Procedure Calls, Diploma thesis (in German), Institute for Scientific Computing, Swiss Federal Institute of Technology, Zurich, Switzerland, 1992

 

Slides

• A note on global induction mechanisms in a µ-calculus with explicit approximations, slides of FICS '02 presentation, Copenhagen, July 20, 2002 (Portable Document Format)

 
• Deductive Model Checking of CTL* Properties, slides of a talk given at the Swedish Institute of Computer Science (SICS), Kista, Sweden, October 9, 2000 (gzipped Postscript, Postscript)