I work in the areas of logic in computer science, cyber-physical systems, programming languages, and formal methods. Below are short descriptions of some of my research topics and directions.
Logic of Dynamical Systems
Logic of dynamical systems studies logics and proof principles for properties of dynamical systems. Dynamical systems are mathematical models describing how the state of a system evolves over time. They are important in modeling and understanding many applications, including embedded systems and cyber-physical systems (CPSs). CPSs combine cyber capabilities (computation and/or communication) with physical capabilities (motion or other physical processes) to solve problems that no part could solve alone. Cars, aircraft and robots are prime examples, because they move physically in space in a way that is determined by discrete computerized control algorithms. Designing these algorithms to control CPSs is challenging due to their tight coupling with physical behavior. At the same time, it is vital that these algorithms be correct, since we rely on CPSs for safety-critical tasks like keeping aircraft from colliding.
"How can we provide people with cyber-physical systems they can bet their lives on?" [Jeannette Wing]
In our group, we develop the logical foundations of cyber-physical systems and study the theory, practice, and applications of logics of dynamical systems and their use in formal verification and validation. This relatively young area is a promising direction for future research, unique in its manifold connections to other pure and applied sciences, including many areas of mathematics, physics, and control theory.
KeYmaera: A Hybrid Theorem Prover for Hybrid Systems
KeYmaera is a hybrid verification tool for hybrid systems that combines deductive, real algebraic, and computer algebraic prover technologies. It is an automated and interactive theorem prover for a natural specification and verification logic for hybrid systems. KeYmaera supports differential dynamic logic (dL), which is a first-order dynamic logic for hybrid programs, a program notation for hybrid systems. KeYmaera supports hybrid systems with nonlinear discrete jumps, nonlinear differential equations, differential-algebraic equations, differential inequalities, and systems with nondeterministic discrete or continuous input. For automation, KeYmaera implements a free-variable sequent calculus and automatic proof strategies that decompose the hybrid system specification symbolically. This compositional verification principle helps scaling up verification, because KeYmaera verifies a big system by verifying properties of subsystems. To overcome the complexity of real arithmetic, we integrate real quantifier elimination and other decision procedures following an iterative background closure strategy. The KeYmaera verification tool is particularly suitable for verifying parametric hybrid systems and has been used successfully for verifying case studies from train control, car control, air traffic control, and robotics.