Dr. Ethan Jackson is a researcher in The Research in Software Engineering (RiSE) Group at Microsoft Research focusing on formal methods for safe cyber-physical systems (CPS). His is the creator of the FORMULA system for formalizing modeling languages and enabling formal analysis of complex software, which has been used in large academic and industrial settings. He is also the co-creator of the P programming language which allows developers to specify complex systems of communicating asynchronous components, and has been used to design critical components of Microsoft Windows. Ethan leads a Microsoft Research program focusing on safe and robust autonomous systems, and has been exploring CPS for disease surveillance. Ethan joined Microsoft Research 2007 after receiving his PhD from Vanderbilt University in Computer Science.

formula formula formula

Formula 2.0

FORMULA 2.0 is framework for formally building domain-specific languages (DSLs) and model transformations.

Project Premonition

Project Premonition seeks to autonomously detect pathogens in animals before they are able to cause outbreaks in people.

The P Language

P is a programming language for protocols and event-driven systems, and provides advanced validation.

Cyber physical systems have a computational core that interacts with the physical world. Proving them safe is scientifically challenging because we must reason about the discrete and the continuous.

- Jeannette Wing
CVP, Microsoft Research

Select Publications

More links and recent press