Curriculum Vitae

Personal Information

Name

Christoph Sprenger

 

Date of birth

January 25, 1967

 

Place of birth

St. Gallen, Switzerland

 

Nationality

Swiss

 

Marital status

unmarried

 

Languages

French, English (both fluently),

German (mother tongue)

 

Current position

Postdoc

 

Current address

INRIA Sophia Antipolis

Projet Lemme

2004, route des Lucioles

BP 93

06902 Sophia Antipolis

France

 

Phone/Fax

+33 492 38 76 93 / +33 492 38 50 60

 

Email

christoph.sprenger@sophia.inria.fr

 

Web

www-sop.inria.fr/lemme/Christoph.Sprenger

 

 

Research Interests

Theory and application of logic in computer science. Formal methods for the design and analysis of computer programs with an emphasis on concurrent and distributed systems.

System and Property Specification

Programming languages and their semantics. Process calculi. Modal and temporal logics including µ -calculi. Type theories and higher-order logic.

 

Proof Techniques

Proof theory of modal and temporal logics. Tableau methods. Abstraction and compositional verification techniques. Inductive reasoning in fixed point logics and type theories. Program synthesis from constructive proofs.

 

Machine-Assisted Reasoning

Deductive and algorithmic techniques. Proof assistants. Proof search, tactics and strategies. Model checking. State space reduction techniques. Tool development.

Education

May 1994--June 2000

Ph.D. (Docteur ès Sciences), Computer Networking Laboratory (LTI), Swiss Federal Institute of Technology (EPFL), Lausanne, Switzerland

Research on a deductive proof system for the verification of temporal properties of infinite-state concurrent systems, including proof of its relative       completeness; also: formal verification of a model checking algorithm for the µ -calculus in a type-theoretic framework; Ph.D. thesis entitled Deductive Local Model Checking -- On the Verification of CTL* Properties of Infinite-State Reactive Systems, supervised by Prof. Claude Petitpierre

 

1986--1992

studies in Computer Science at the Swiss Federal Institute of Technology (ETH), Zurich, Switzerland

specialisation in computer architecture, compiler construction, operating systems and control theory; diploma thesis entitled Network Computing with Non-Blocking Remote Procedure Calls (in German), supervised by Prof. W. Gander and Dr. P. Arbenz

 

1981--1985

Gymnasium, Heerbrugg, Switzerland; Matura Type B

 

 

Professional/Research Experience

October 2002-present

postdoctoral position in the Lemme project at the INRIA Sophia Antipolis, France, supported by an ERCIM fellowship, group leader: Dr. Gilles Barthe

research on automated compositional verification of control flow based security properties of multi-application JavaCard programs, in collaboration with Marieke Huisman (INRIA) and Dilian Gurov (KTH, Sweden) in the context of the EU project VerifiCard

 

August 2001-August 2002

postdoctoral position in the Formal Design Techniques Group at the Swedish Institute of Computer Science (SICS), Kista, Sweden, supported by Swiss European Fellowship No. 83EU-065536 (attributed by Swiss NSF), group leader: Prof. Mads Dam

research on proof systems for fixed point logics (µ -calculi), focus on mechanisms supporting inductive reasoning in tree-shaped and cyclic proofs, in collaboration with Mads Dam

 

July 2000--May 2001

postdoctoral position at the Computer Networking Laboratory (LTI), EPF Lausanne, Switzerland, lab leader: Prof. Claude Petitpierre

prototype implementation of the proof system developed in my Ph.D. thesis, consists of a front-end for the construction of temporal tableaux and a back-end theorem prover (PVS, SRI International) to prove the first-order side conditions generated during the tableau construction

 

June 1992--March 1994

scientific collaborator at the Institute for Scientific Computing at ETH Zurich in the group of Prof. Walter Gander and Dr. Peter Arbenz

revision and extension of the Sciddle remote procedure call package including port to Cray and Nec supercomputers, case study

Teaching Experience

May 1994--May 2001

(at EPFL) tutor for practical programming exercises of the course ``Programmation I'' taught by Prof. Petitpierre during each winter term

 

October 1995

(at EPFL) lesson on ``Temporal Logic for Reasoning about Concurrent Programs'' in the context of Module M7 ``Communication Software Engineering'' of the ``Postgraduate Course on Communication Networks''

Supervising Experience

Summer Term 1996

(at EPFL) Julien Brunet, 8th term Mathematics student, term project entitled "Un modèle pour les calculs de processus" and Vincent Graf, 8th term Mathematics student, term project entitled "Un modèle asynchrone de vérification modulaire"

 

Winter Term 1994-95

(at EPFL) Thomas Portmann, Computer Science student, diploma project on "Objets SyncC++ réalisant des RPC"

Research Visits

April--May 2003 (1 week)

working visit at Swedish Institute of Computer Science (SICS), collaboration with Dr. Dilian Gurov, talk at KTH on ``Refinement, Modal Equation Systems and Compositional Verification''

 

April 2001 (3 days)

visitor of Prof. Michael Fisher's Logic and Computation Group at the University of Liverpool, United Kingdom; talk on ``Games and Deductive Model Checking for CTL*''

 

October 2000 (1 week)

visit including presentation at the Swedish Institute of Computer Science (SICS), Kista, Sweden, group of Dr. Mads Dam

 

January 1998 (1 week)

visitor and talk in the group of Prof. Dr. Henrik Reif Andersen at the IT University, Lyngby, Denmark

 

Mid May 1997 (3 days)

visitor and talk in the Coq project group (invited by Dr. Hugo Herbelin) at INRIA Rocquencourt, France

 

Sept.--Oct. 1992 (5 weeks)

visitor in the group of Prof. Dr. Jack Dongarra at the University of Tennessee, Knoxville, Tennessee; talk at the ``Parallel Circus'' meeting, October 30-31, North Carolina Supercomputing Center, Durham, North Carolina

Publications

Submitted Articles

[1]

Ch. Sprenger, Dilian Gurov and Marieke Huisman, Simulation Logic, Applets and Compositional Verification, submitted to ACM Symposium on Principles of Programming Languages, POPL 04, July 2003

Conference and Workshop Articles (refereed)

[2]

Ch. Sprenger and K. Worytkiewicz, A verification methodology for infinite-state message passing systems, Proceedings of 1st ACM & IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2003), Mont-Saint-Michel, France, June 24-26, 2003

 

[3]

Ch. Sprenger and M. Dam, On the structure of inductive reasoning: circular and tree-shaped proofs in the µ -calculus, In Foundations of Software Science and Computation Structures, FoSSaCS '03, Lecture Notes in Computer Science 2620, pp. 425--440, 2003

 

[4]

Ch. Sprenger and M. Dam, A note on global induction mechanisms in a µ -calculus with explicit approximations, Workshop on Fixed Points in Computer Science, FICS '02, Copenhagen, July 20-21, 2002

 

[5]

Ch. Sprenger, 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, Lecture Notes in Computer Science, Vol. 1384, pp. 167--183, Springer-Verlag, 1998

 

[6]

P. Arbenz, K. Gates and Ch. Sprenger, A parallel implementation of the symmetric tridiagonal QR algorithm, Proceedings of the 14th Symposium on the Frontiers of Massively Parallel Computation, McLean, Virginia, October 19-21, 1992

Journal Articles

[7]

Ch. Sprenger and M. Dam, A note on global induction mechanisms in a µ -calculus with explicit approximations, journal version of [4], accepted for publication in RAIRO Theoretical Informatics and Applications, July 2003

 

[8]

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

Technical Reports

[9]

Ch. Sprenger, Dilian Gurov and Marieke Huisman, Simulation Logic, Applets and Compositional Verification, full version of [1], INRIA Technical Report RR-4890, July 2003

 

[10]

Ch. Sprenger, User's Guide to Sciddle 3.0, CS Report No. 208, Dept. of Computer Science, ETH Zurich, Switzerland, December 1993

Theses

[11]

Ch. Sprenger, 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

 

[12]

Ch. Sprenger, Network Computing with Non-Blocking Remote Procedure Calls, Diploma Thesis (in German), Swiss Federal Institute of Technology, Zurich, Switzerland, 1992