Project Systems

CURRICULUM VITAE

Stavros Tripakis

November **, 2009

**** ********* ****** +1-510-***-**** (cell)

Berkeley, CA 94703 *******.********@*****.***

RESEARCH INTERESTS

Modeling, analysis and implementation of embedded systems. Verification and synthesis.

Testing and

fault diagnosis. Component-based design. Concurrent, distributed and multicore systems.

EMPLOYMENT

02/2009present: Visiting Associate Research Scientist, University of California,

Berkeley.

01/2000present: Research Scientist ( Charge de Recherche ), CNRS ( Centre National

de la'

Recherche Scientifique ), Verimag Laboratory, France.

(Currently on leave.)

02/200611/2008: Research Scientist, Cadence Research Laboratories, Cadence Design

Systems,

Inc., Berkeley, CA, USA

.

05/200005/2001: Visiting Assistant Research Engineer, California PATH (Partners for

Automated

Transit and Highways), Caltrans and University of California, Berkeley

.

02/199905/2000: Visiting Scholar, Electronics Research Laboratory, University of

California,

Berkeley.

09/199012/1993: Research Assistant at the Computer Science Institute, Foundation of

Research

and Technology, Hellas, Heraklion, Greece.

EDUCATION

10/199512/1998: PhD in Computer Science, Joseph Fourier University, Grenoble,

France.

Dissertation: The formal analysis of timed systems in practice.

Advisor: Dr. Joseph Sifakis (Turing Award 2007).

'

10/199407/1995: M.S. in Computer Science and Mathematics, Ecole Normale Superieure

of Paris,'

'

Ecole Polytechnique, Universities of Paris VI, VII and XI.

1

10/198812/1993: Bachelor degree and postgraduate studies in Computer Science and

Mathematics,

University of Crete at Heraklion, Greece.

CONSULTANCIES AND INTERNSHIP

10/200412/2004: Consultant for RATP (the Paris subway operator), France

.

09/200001/2001: Consultant for Terablaze Inc., Cupertino, CA, USA.

07/199608/1996: Summer intern, Bell Labs, Murray Hill, NJ, USA.

AWARDS AND HONORS

Technical Program Committee Co-Chair: Embedded Software EMSOFT 2010.

Paper [16] received the Distinguished Paper Award.

Nominated and elected Secretary/Treasurer of ACM SIGBED (Association for Computing

Machinery

Special Interest Group on Embedded Systems), July 2009 June 2011.

Jury compliments ( Felicitations du jury ) for my PhD thesis. Given to less than 5%

of theses'

defended at Joseph Fourier University each year.

PhD scholarship (

1995-1998) by the French Ministry of Education

.

International student scholarship (

1994-1995), Ecole Polytechnique, France

.

Erasmus scholarship (

1/1994-6/1994), University of Paris VI, France.

First in my class (

1988-1992), and graduate scholarship (1992-1994), University of

Crete, Greece.

RESEARCH GRANTS AND PROJECTS

Proposals submitted while at UC Berkeley (since 02/2009):

Proposal Algorithmic Synthesis for System Design submitted to NSF Expeditions in

Computing Pro-

gram, 09/2009. Co-author and Investigator.

Proposal Fundamentals of Networked Software Dynamics submitted to ONR Fundamentals of

Cy-

berspace and Software Program, 08/2009. Co-author and Investigator.

Proposal Timing-Centric Software submitted to NSF Cyber Physical Systems Program,

02/2009. Co-

author and Investigator

.

Proposals submitted and funded while at

Verimag, France (20012006

):

1/20022/2004: European IST project NEXT TTA High-Confidence Architecture for

Distributed

Control Applications. Verimag PI.

2

8/20022/2005: European IST project RISE Reliable Innovative Sofware for Embedded

Systems.

Verimag co-PI.

9/2003 9/2006: Research grant recipient by the Rhone-Alpes region on Design and

implementation

of embedded software components. Funding provided for my PhD student Christos Sofronis.

9/20049/2005: Research contract with RATP (the Paris subway operator) on the

verification of a

subway signaling station. Co-PI.

7/20046/2005: Recipient of a young researcher grant by CNRS.

9/2003 9/2006: French project CORTOS Control and Observation of Real-Time Open

Systems.

Verimag PI.

1/200512/2005: French project Emtest Testing of embedded systems. Co-PI.

1/2002 12/2002: French project eKronos Timing analysis of embedded software. Co-PI.

9/2003 9/2004: France-Berkeley Fund project Service Networks Intelligent middleware for

dis-

tributed applications. Co-PI.

Member of the Artist Network of Excellence on Embedded Systems (2001 2006). Verimag

PI for the

Testing and Verification Cluster and the Distributed and Real-Time Observation and

Control Activity.

Participation in projects at UC Berkeley (during post-doc, 1999 2001):

DARPA projects MoBIES Model Based Integration of Embedded Systems and Smart Networks,

and

in ONR project Distributed Autonomous Agent Networks.

PATENTS

Method, system and computer program product for implementing external domain

independent model-

ing framework in a system design, with Yaron Kashai and Felice Balarin, filed on

12/28/2007, number

CA7058312001.

Method and system for verifying electronic designs having software components, with Ken

McMillan,

filed on 12/21/2007, number CA7057221001.

Generating modular and hierarchical execution code from untimed and timed block

diagrams, with

Roberto Lublinerman, filed on 09/07/2007, number CA7056892001.

STUDENTS AND POSTDOCS

98). Undergraduates: Cyril Guironnet

(Spring 05),

Rachid Mokhtari (Spring 05), Nguyen Quang-Trung (Spring 05), Mohamed Dergueche

(Spring 05),

Emile Verdurae (Spring 04), Jamel Hajji (Spring 04), Maher Sebai (Spring 04).

At Cadence Labs: Roberto Lublinerman (intern, summers 07 and 08), Jochen Zimmerman

(intern,

Mar 08 - Sep 08), Tobias Welp and Yang Yang (UC Berkeley EE 249 class project, Fall 07).

Member of the Ph.D. thesis jury of:

Sarah Zennou, Partial-order verification methods for timed automata, Marseille

University, France,

2004.

Guillaume Gardey, Verification methods for timed Petri nets, Rennes University, France,

2005.

Emilie Oudot, Contributions to the incremental verification of composite timed systems,

Franche-

Comte University, France, 2006.'

TEACHING

Fall 2009: One 1.5 hour lecture given in graduate course CE 290I Civil Systems:

Control and In-

formation Management, Civil And Environmental Engineering Department, University of

California,

Berkeley.

Fall 2009, Fall 2007, and Fall 2006: Total of five 1.5 hour lectures given in graduate

course EE

249 Design of Embedded Systems: Models, Validation and Synthesis, Electrical

Engineering and

Computer Sciences Department, University of California, Berkeley.

Spring 2009: Two 1.5 hour lectures given in undergraduate course EE 149 Introduction

to Embed-

ded Systems, Electrical Engineering and Computer Sciences Department, University of

California,

Berkeley.

Spring 2005: co-taught graduate course Testing Methods, Joseph Fourier University,

Grenoble, France.

4

Fall 1999: co-taught undergraduate course EE 122 Introduction to Communication

Networks, Uni-

versity of California, Berkeley.

Spring 1996: taught graduate course Formal Methods and Verification, University of

Crete, Heraklion,

Greece.

ADVISORY ROLES AND OTHER PROFESSIONAL ACTIVITIES

Technical Program Committee Co-Chair: Embedded Software EMSOFT 2010.

Associate Editor, Journal of Discrete Event Dynamic Systems (01/2010 12/2012).

Member of Cadence Strategic Option Analysis and Market Segment Analysis teams, and

Cadence

Research Operations Committee, 10/2006 10/2008.

Project Evaluator for European Framework Program 7, Objective: Embedded Systems Design,

4-7

June 2007.

Project Reviewer of European IST project COLUMBUS Design of Embedded Controllers for

Safety

Critical Systems, 07/2002 06/2004.

Organizing Committee Member:

Workshop on Control and Observation of Real-Time Open Systems (CORTOS 2006), Satellite

workshop of the 17th International Conference on Concurrency Theory (CONCUR 2006).

(CDC). Hybrid Systems: Computation and Control (HSCC). Formal Methods in Computer-Aided

Design (FMCAD). International Colloquium on Automata, Languages and Programming (ICALP).

Verification, Model Checking, and Abstract Interpretation (VMCAI). Application of

Concurrency to

System Design (ACSD). Formal Modelling and Analysis of Timed Systems (FORMATS). Workshop

on Discrete Event Systems (WODES). Formal Techniques for Networked and Distributed

Systems

(FORTE). Runtime Verification (RV). Euromicro Conference on Real-Time Systems (ECRTS).

TECHNICAL PROGRAM COMMITTEE MEMBER

13th International Conference on Hybrid Systems: Computation and Control (HSCC 2010).

Also

HSCC 2009 and 2001.

10th International Workshop on Discrete Event Systems (WODES 2010). Also WODES 2008.

Design, Automation and Test in Europe (DATE 2010), Technical Track on Model Based

Design of

Embedded Systems. Also DATE 2008 and 2007, same track.

30th IEEE Real-Time Systems Symposium (RTSS 2009) Design and Verification of Embedded

Real-Time Systems Track.

IEEE Symposium on Industrial Embedded Systems (SIES 2009).

7th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS

2009). Also FORMATS 2008, 2007, 2005 and 2003.

21st International Conference on Computer Aided Verification (CAV 2009).

10th International Workshop on Verification of Infinite-State Systems (INFINITY 2008).

28th IFIP WG6.1 International Conference on Formal Techniques for Networked and

Distributed

Systems (FORTE 2008).

DATE 2008 Workshop on Dependable Software Systems.

23rd Annual ACM Symposium on Applied Computing (SAC 2008), Technical Track on Embedded

Systems: Applications, Solutions, and Techniques.

8th Workshop on Runtime Verification (RV 2008).

3rd intl Workshop on Systems Software Verification (SSV 2008).

7th ACM International Conference on Embedded Software (EMSOFT 2007).

13th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS 2007).

6

16th Euromicro Conference on Real-Time Systems (ECRTS 2004).

3rd International Conference on Application of Concurrency to System Design (ACSD

2003).

Workshop on Real-Time Tools (RT-TOOLS 2002). Also RT-TOOLS 2001.

INVITED TALKS

Model-Based Design: Semantics-Preserving Implementation of Synchronous Models. Dagstuhl

Sem-

inar on Synchronous Languages (SYNCHRON 09). Nov 22-27, 2009, Dagstuhl, Germany.

Relational Interfaces, University of California, Los Angeles, Sep 25, 2009.

Implementation of Synchronous Programs on Asynchronous Execution Platforms:

Correctness, Mod-

ularity, and Performance Analysis. Caltech Workshop on Verification and Validation, Sep

23-24,

2009, Pasadena, CA.

Correct and Efficient Implementations of Synchronous Models on Asynchronous Execution

Platforms .

2

CAV 2009 Workshop on Exploiting Concurrency Efficiently and Correctly (EC), Jun 26-27,

2009,

Grenoble, France.

Model-Based Design: Semantics-Preserving Implementation of Synchronous Models. CS

Depart-

ment, Iowa State University, Mar 5, 2009, Ames, IA.

Implementing Synchronous Models on Distributed Execution Platforms. CHESS Seminar,

University

of California, Berkeley, Feb 24, 2009, Berkeley, CA.

Modular Code Generation from Synchronous Block Diagrams: Modularity vs. Reusability vs.

Code

Size. CHESS Seminar, University of California, Berkeley, Feb 3, 2009, Berkeley, CA.

Modular Code Generation from Synchronous Block Diagrams. Department of Information

Technol-

ogy, Uppsala University, Dec 15, 2008, Uppsala, Sweden.

Modular Code Generation from Synchronous Block Diagrams. 3rd International Workshop on

Foun-

dations and Applications of Component-based Design (WFCD2008). ArtistDesign Workshop orga-

nized within Embedded Systems Week, Oct 19, 2008, Atlanta, GA.

Research Problems in Embedded Distributed Systems, GSRC (Gigascale Systems Research

Center)

Workshop on Distributed Systems, Sep 22, 2008, Berkeley, CA.

Modular Code Generation from Synchronous Block Diagrams. CAV 08 Workshop on Numerical

Abstractions for Software Verification (NSV 08), Jul 8, 2008, Princeton, NJ.

Monitoring, Fault Diagnosis and Testing Real-time Systems using Analog and Digital

Clocks. Dagstuhl

Seminar on Runtime Verification, Jan 4, 2007, Dagstuhl, Germany.

Black-box Conformance Testing for Real-Time Systems. LIAFA Laboratory (Laboratoire

d Informatique

Algorithmique: Fondements et Applications), University of Paris 7, Nov 11, 2005, Paris,

France.

7

Testing and Fault-Diagnosis for Real-Time Systems. Artist2 Summer School on Component &

Mod-

elling, Testing & Verification, and Statical Analysis of Embedded Systems, Oct 2, 2005,

Nasslingen,

Sweden.

Undecidable Problems in Decentralized Observation and Control. Department of Computer

Science

Seminar Series, Universite Libre de Bruxelles, May 19, 2005, Brussels, Belgium.'

An Expressive and Implementable Formal Framework for Testing Real-Time Systems. Artist

European

Project Meeting, Feb 2005, Oldenburg, Germany.

Testing Real-Time Systems. LAAS Laboratory (Laboratoire d Analyse et d Architecture des

Sys-

temes), May 4, 2004, Toulouse, France.

Testing Real-Time Systems. NASA Ames Research Center, Mar 11, 2004, Moffett Field, CA.

Implications of the Undecidability of the Universality Problem for Timed Automata.

Workshop of

the CNRS STIC Project on Automata, Distributed and Timed Models, Verimag Laboratory, Mar

10,

2003, Grenoble, France.

Undecidable Problems in Decentralized Observation and Control. Workshop on Automata,

Dis-

tributed and Timed Models, LaBRI Laboratory (Laboratoire Bordelais de Recherche en

Informatique),

Nov 7, 2002, Bordeaux, France.

Fault-Diagnosis of Timed Systems, BRICS Seminar Series, Department of Computer Science,

Aalborg

University, Aug 6, 2002, Aalborg, Denmark.

Protocol Design and Verification. Workshop on Networked Autonomous and Semi-autonomous

Ve-

hicles, IEEE Conference Decision and Control (CDC 01), Dec 3, 2001, Orlando, FL.

Undecidable Problems in Decentralized Observation and Control. Workshop on Recent

Advances in

Discrete-Event Systems, Sep 7, 2001, Ann Arbor, MI.

Panelist in Hybrid System Applications: An Oxymoron?, Panel of the Intl. Conf. on

Hybrid Systems:

Computation and Control, Mar 30, 2001, Rome, Italy.

SOFTWARE

I developed or contributed to the development of the following tools that are publicly

distributed. The

web pages of the tools are accessible from http://www-verimag.imag.fr/~tripakis/.

Developer of RT-Spin, an extension of the Spin model-checker for real-time.

Developer of Minim, a minimization tool for timed automata.

One of four developers of Kronos, a model-checker for timed automata.

Developer of Open-Kronos, an extension of the SMI model-checker for timed automata.

Coordinator of the development of the Simulink/Stateflow-to-Lustre translator

(developed by PhD

student Christos Sofronis and post-doc Norman Scaife).

8

Supervised the development of the Simulink modular code generator (developed by PhD

student

Roberto Lublinerman, not publicly available).

PROGRAMMING AND MODELING

C, C++, Java, Haskell, Smalltalk, Nvidia CUDA, SystemC, Matlab, Simulink/Stateflow, Spin,

SMV,

Ptolemy.

PROFESSIONAL ORGANIZATIONS

ACM (Association for Computing Machinery), ACM SIGBED (Special Interest Group on Embedded

Systems). Secretary/Treasurer of ACM SIGBED, July 2009 June 2011.

LANGUAGES

Greek, native. English, fluent. French, fluent. Finnish, basic.

CITIZENSHIP AND IMMIGRATION STATUS

Greek citizen. US permanent resident (green card).

9

LIST OF PUBLICATIONS

The PDF file has links to on-line versions of the papers below. My papers are also

accessible on-line

~

from http://www-verimag.imag.fr/ tripakis/.

REFEREED JOURNAL PAPERS

REFEREED CONFERENCE PAPERS

[95] C. Courcoubetis and S. Tripakis. Probabilistic model checking: formalisms and

algorithms for discrete

and real-time systems. In Verification of Digital and Hybrid Systems (M.K. Inan and R.P.

Kurshan,

eds.), NATO ASI Series F: Computer and Systems Sciences, Vol. 170, 2000.

THESES

[96] S. Tripakis. The Formal Analysis of Timed Systems in Practice. PhD thesis,

Universite Joseph Fourrier'

de Grenoble, France, 1998.

[97] S. Tripakis. Minim: a Tool for Minimization of Timed Automata with respect to Time

Abstracting

Bisimulations. Master s thesis, Ecole Normale Superieure de Paris, Ecole Polytechnique

and Univer-'

site de Paris, France, 1995.'

19

Contact this candidate