Mark-Oliver Stehr

Address:

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

Raum:

EL-286

Telefon:

1-650-859-5710

Telefax:

1-650-859-2844

E-Mail:

stehr@csl.sri.com

Stellung:

Computer Scientist

Zuvor:

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)

Bibliographie

Aktuelle Vorträge:

• 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.

Projekte:

• 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
• Formale Spezifikation einer Programmiersprache für aktive Netzwerke
• OCC - Offenenes Kalkül der Konstruktionen (open calculus of constructions)
• Reine Typ Systeme (Pure Type Systems) in Rewriting Logik
• CINNI - Ein Kalkül der indizierten Namen und benannten Indizes
• Termersetzungs-Semantik (rewriting semantics) für höhere Petri-Netze
• Formale Interoperabilität beim rechnergestützten Theorembeweisen
• Spezifikation und Verifikation im Rahmen der Typtheorie

Alte Projekte:

• Allgemeine Netztheorie (in German only)
• Zyklische Ordnungen
• Theorie der Nebenläufigkeit (Concurrency Theory)
• Modelling And Analysis Of Time Constrained And Hierarchical Systems (MATCH)

Wissenschaftliche Veranstaltungen

• 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)

Seminare und Vorlesungen

• Vorlesung: Typtheorie (SS 97 und WS 01/02)
• Projektseminar: Rechnergestueztes Beweisen (WS 97/98)
• Vorlesung: Allgemeine Netztheorie (SS98, siehe auch hier)
• Projektseminar: Formale Verifikation verteilter Algorithmen (SS 98)
• Vorlesung: Assertional Reasoning and Temporal Logic for System Verification
  MATCH Advanced Summer School, Jaca, Spain, September 98