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). He asks: "How can we engineer safer autonomous systems, and are there autonomous systems that make us safer?".

He leads Project Premonition, an advanced research program which aims to detect the movements of potential pathogens in the environment, before they cause outbreaks in humans. This system employs drones, robotic mosquito traps, and metagenomics to find, collect, and analyze mosquitoes for both known and unknown viruses. It also collects big data on mosquito behavior to better inform epidemiological models and public health organizations. This project is part of the Microsoft Research Expeditions Program.

Ethan 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 joined Microsoft Research 2007 after receiving his PhD from Vanderbilt University in Computer Science.


Project Premonition

Established: March 2, 2015

Interested in evaluating Project Premonition technologies and data? Sign up here Project Premonition aims to detect pathogens before they cause outbreaks Emerging infectious diseases such as Zika, Ebola, Chikungunya and MERS are dangerous and unpredictable. Public health organizations need data as early as possible to predict disease spread and plan responses. Yet early data is very difficult to obtain, because it must be proactively collected from potential disease sources in the environment. Researchers estimate between…

FORMULA – Modeling Foundations

Established: December 10, 2008

FORMULA 2.0: Formal Specifications for Verification and Synthesis Formula specifications are highly declarative logic programs that can express rich synthesis and verification problems. FORMULA 2.0 is framework for formally specifying domain-specific languages (DSLs) and model transformations. FORMULA specifications are succinct descriptions of DSLs, and specifications can be immediately connected to state-of-the-art analysis engines without additional expertise. FORMULA provides: (1) succinct specifications of DSLs and compilers, (2) efficient compilation and execution of input programs, (3) program…