Mark-Oliver Stehr

Address:

SRI International - Computer Science Laboratory
333 Ravenswood Avenue, Menlo Park, CA 94025, USA

Room:

EL-286

Phone:

1-650-859-5710

Telefax:

1-650-859-2844

E-Mail:

stehr@csl.sri.com

Position:

Computer Scientist

Previously:

Postdoctoral Research Associate at University of Illinois at Urbana-Champaign, Computer Science Department, Urbana-Champaign, Illinois, USA

International Fellow at SRI International, Computer Science Laboratory, Menlo Park, California, USA

Visiting Scholar at Stanford University, Computer Science Department, Stanford, California, USA

Research Assistant at Universität Hamburg, Fachbereich Informatik, Hamburg, Germany

Funding:

• RIDE: Robust Internetworking in Disruptive Environments (DARPA)
• CONTESSA: Addaptive System Interoperability (ONR)

Bibliography

Recent Talks:

• RIDE - Robust Internetworking in Disruptive Environments (University of Illinois at Urbana-Champaign, University of California, Santa Cruz and SRI International) . DARPA Disruption-Tolerant Networking (DTN) Kickoff meeting. March 1, Washington, DC.
• Practical Techniques for Language Design and Prototyping (joint work with Carolyn Talcott). Dagstuhl Seminar on Foundations of Global Computing . Schloss Dagstuhl, February 20 - 26, Germany (slides available in ppt, pdf, and pdf with four slides per page).
• The Open Calculus of Constructions and its Semantics . Talk at the 2nd Workshop on Coq and Rewriting September 22 - 24 2004, LIX, Palaiseau, France (slides available in ppt and pdf).
• The Open Calculus of Constructions as a Tool for Inductive and Coinductive Specification and Reasoning . Invited talk at the Workshop on Algorithms and Tools for Coinductive Reasoning, September 16 - 22, 2004, Dresden, Germany (slides available in ppt and pdf).
• Higher-Order Rewriting via Conditional First-Order Rewriting in the Open Calculus of Constructions . Invited talk at HOR'2004, June 2, Aachen, Germany (available in ps and pdf).
• Synthesis of Generalized Ring Protocols Using Concepts of Special Relativity Theory. Stevens Institute of Technology, Hoboken, New Jersey. Stevens Computer Science Seminar, May 3, 2004. Selection of slides from the Monterey talk (available here and here).
• Concurrent Broadcasting Schemes for Wireless Networks: Applying Formal Tools and Concepts of Special Relativity Theory. University of Pennsylvania, Philadelphia. Security Lab Seminar, April 30, 2004. Selection of slides from the Monterey talk (available here and here).
• Concurrent Broadcasting Schemes for Wireless Networks. Protocol Exchange Meeting at Naval Postgraduate School, Center for Information Systems Security Studies and Research, February 9-11, 2004, Monterey, California. Slides available here and here.
• Cyclic Orders: A Foundation for Concurrent Synchronization Schemes. University Paris 7, Group Preuves, Programmes et Systemes, December 16, 2003. Part I: Thinking in Cycles, Part II: Concurrent Broadcasting Schemes for Wireless Networks.
• The Open Calculus of Constructions: A Framework for Executable Mathematics. Ecole Polytechnique, Laboratoire d'Informatique - LIX, December 12, 2003, Paris. Slides available here.
• Towards an Execution Environment for the MSR Cryptoprotocol Specification Language (joint work with Iliano Cervesato, ITT Industries). Contessa Review Meeting 2003, December 5, 2003, University of Pennsylvania. Slides available here.
• Application of Maude: Group Communication and Security. UMBC Protocol Analysis Meeting, October 1-2, 2003, Baltimore. Slides available here.
• Composable Formal Models for High-Assurance Fault Tolerance Networks (joint work with C. L. Talcott). FTN PI Meeting, July 21-23, 2003, Honolulu, Hawaii. Conference site here.
• On the Significance of Formal Methods in the Development of High-Assurance Secure Systems. Invited Lecture at the Naval Postgraduate School, Center for Information Systems Security Studies and Research, July 30, 2003, Monterey, California. Lectures archive here.
• Formal Specification of Sectrace (joint work with A. Sridharanarayanan). Workshop on Context Sensitive Systems Assurance (Contessa'03), April 1, 2003, Philadelphia. Project site here
• Formal Specification of Group Communication Middleware (joint work with C. L. Talcott). Workshop on Context Sensitive Systems Assurance (Contessa'03), April 1, 2003, Philadelphia. Project site here
• Relating the MSR Crypto-Protocol Specification Language to Rewriting Logic with Dependent Types. UMBC Protocol Analysis Meeting, June 10-11, 2003, Baltimore. Slides available here.
• Tutorial: Explicit Substitutions and the Open Calculus of Constructions . Given at WRLA'2002, 4th International Workshop on Rewriting Logic and its Applications, Pisa, Italy, September 19--21, 2002.
• On the Rewriting Logic Approach to Colored Net Specifications . Given at Universita di Pisa, Dipartimento di Informatica, September 18, 2002.

Projects:

• An Execution Environment for the MSR Cryptoprotcol Specification Language
• Specification of the Group Diffie-Hellman Protocol as a Component of the Cliques Toolkit
• Modular Specification of a Group Communication System
• Specification and Analysis the Sectrace and L3A Protocols
• Formal Specification of an Active Network Programming Language
• OCC - Open Calculus of Constructions
• Pure Type Systems in Rewriting Logic
• CINNI - A Calculus of Indexed Names and Named Indices
• Rewriting Semantics for High-Level Petri Nets
• Formal Interoperability in Computer-Aided Theorem Proving
• Specification und Verification in A Type Theoretic Framework

Old Projects:

• General Net Theory (in German only)
• Cyclic Orders
• Concurrency Theory
• Modelling And Analysis Of Time Constrained And Hierarchical Systems (MATCH)

Scientific Events

• RTA'2005 - International Conference on Rewriting Techniques and Applications (Nara, Japan)
• CONTESSA Workshop 2004 - Adaptive Systems Interoperability (Irvine, California)
• VCL'2002 - Verification and Computational Logic (Pittsburgh, Pennsylvania)
• PNSE'97 - Petri Nets in System Engineering (Hamburg, Germany)

Seminars and Lectures

• Lecture: Type Theory (SS 97 and WS 01/02)
• Projectseminar: Computer-Aided Theorem Proving (WS 97/98)
• Lecture: General Net Theory (SS98, see also here)
• Projectseminar: Formal Verification of Distributed Algorithms (SS 98)
• Lecture: Assertional Reasoning and Temporal Logic for System Verification
  MATCH Advanced Summer School, Jaca, Spain, September 98