Autonomous Systems Verification and Validation.

Developed the first deep neural networks for guiding proof search.

https://scholar.google.com/citations?user=9j79kA8AAAAJ&hl=en

Thesis: Differential Refinement Logic

• CMU School of Computer Science Dissertation Award, runner up, 2016

• National Science Foundation (NSF) Graduate Research Fellowship Program, 2009-2011

• U.S. Department of Energy (DOE) Computational Science Graduate Fellowship (CSGF), 2011-2014

• Young Researcher Award, Heidelberg Laureate Forum, 2013

• National Defense Science and Engineering Graduate Fellowship (NDSEG), 2009

Topic: Formal Verification of Cyber-Physical Systems

Developed new methods to formally verify safety-critical cyber-physical systems, like computer-controlled cars and aircraft. Created Differential Refinement Logic for connecting abstract models to more concrete implementations, enabling verification of more challenging systems, modular proof structure, and iterative system design. Defined provable refinement relations between event-driven and time-triggered controls systems. Developed relationships between refinable open-loop control envelopes and closed-loop safety requirements.

Faculty hiring committee (one of six members), Ph.D. admissions committee.

https://cs.cmu.edu/~sloos