Luca de Alfaro Assistant Professor Computer Engineering Department Jack Baskin School of Engineering University of California, Santa Cruz Office: E2, 339A Phone: (831) 459-4982 Fax: (831) 459-4829 WWW: http://www.soe.ucsc.edu/~luca

Interests

• Formal methods for system design and verification.
• Interface specifications for component-based design.
• Embedded software design.
• Modeling and analysis of systems: reactive, hybrid, and stochastic.
• Model checking.
• System interaction: game theory, concurrency theory.

Research

Recent Work

• L. de Alfaro, M. Faella, T.A. Henzinger, R. Majumdar, M. Stoelinga. Model Checking Discounted Temporal Properties. To appear in Theoretical Computer Science, Elsevier. Postscript, PDF.
• L. de Alfaro, T.A. Henzinger. Interface-Based Design. In Engineering Theories of Software Intensive Systems, proceedings of the Marktoberdorf Summer School, Kluwer, 2004. Postscript, PDF.
• K. Chatterjee, L. de Alfaro, and T.A. Henzinger. Trading Memory for Randomness. In QEST 04: 1st International Conference on the Quantitative Evaluation of Systems, 2004. Postscript, PDF.
• L. de Alfaro, P. Godefroid, R. Jagadeesan. Three-Valued Abstractions of Games: Uncertainty, but with Precision. In LICS 04: Proceedings of 19th IEEE Symposium on Logic in Computer Science, 2004. Postscript, PDF.
• L. de Alfaro, M. Faella, M. Stoelinga. Linear and Branching Metrics for Quantitative Transition Systems. In ICALP 04: 31st International Colloquium on Automata, Languages, and Programming, LNCS, Springer-Verlag, 2004. Postscript, PDF.
• L. de Alfaro, M. Faella, T.A. Henzinger, R. Majumdar, M. Stoelinga. Model Checking Discounted Temporal Properties. In TACAS 2004: 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, LNCS, Springer-Verlag, 2004. Postscript, PDF.
• L. de Alfaro, R. Majumdar. Quantitative Solution of Omega-Regular Games. In Journal of Computer and System Sciences 68, pages 374-397, 2004. Postscript, PDF. A preliminary version of this paper appeared in STOC 01: 33rd Annual ACM Symposium on Theory of Computing, 2001.

Conferences

I am involved in the following upcoming conferences:

• EMSOFT 2005: ACM Conference on Embedded Software, Jersey City, USA, 2005.
• LICS 2005: 20th Annual IEEE Symposium on Logic in Computer Science, Chicago, USA, 2005.
• CBSE 2005: International Symposium on Component-Based Software Engineering, St. Luis, Missouri, USA, 2005.
• FINCO 2005: Workshop on Foundations of Interactive Computing, Edinburgh, Scotland, 2005.

Talks

• Qualitative Verification and Control via the mu-calculus (CONCUR 2003 invited talk, September 2003).
• Games as Types for Component-Based Design (FOCLASA 2003 invited talk, September 2003)
• Formal Methods for Component-Based Design (Summer Research Institute, EPFL, July 2003).
• Modeling Open Systems as Games (International Symposium on Verification, Taormina, June 2003).
• Interfaces for Component-Based Design (NISA meeting, San Jose, June 2003).
• Games and Fixpoint Logics (Workshop on Mathematical Models, Montreal, October 2002).
• Behavioral Component Interfaces (First CUE Workshop, Macau, October 2002).
• Timed Interfaces (EMSOFT, October 2002). Talk by Mariëlle Stoelinga.
  More talks

Teaching

Spring 2005: CMPE 016: Discrete Math

Past:

• CMPE 016 - Discrete Mathematics: Spring 2004.
• CMPE 117 - Embedded Software: Spring 2002, Spring 2003, Winter 2004, Winter 2005.
• CMPE 276 - Software Engineering: Fall 2002.
• CMPE 278 - Introduction to Discrete-Systems Theory: Fall 2003, Fall 2004.
• CMPE 293 - Fall 2001 topic: Introduction to Discrete-Systems Theory: Fall 2001.

Contact Information

• Mailing address
• Travel schedule
• Directions to the School of Engineering
• Directions to the Silicon Valley Center
• Office Hours: Mondays 1-2, or by appointment. See also the travel schedule.

Research Group

• Marco Faella (postdoc)
• Maria Sorea (postdoc)
• Vishwanath Raman (Ph.D. student)
• Pritam Roy (Ph.D. student)
• Leandro Dias Da Silva (visiting student)

Former Postdocs

• Mariëlle Stoelinga

Information for prospective students and visitors.

Software

• robos, my version of the LegOS operating system.

Miscellaneous

• Is my last name under 'A' or 'D'?
• Emacs fill-sentence macro.
• My personal page
• Françoise Beaufays