A key challenge in computer science research is to establish that systems, algorithms, programs, and compilers behave correctly. We tackle this challenge by showing that a formal description of a program or a system exhibits a set of well-defined properties through research that involves algorithms, complexity, logic, and semantics.
Approaches to this challenge vary:
This theme is closely related to our Mathematical Foundations of Software theme, but focuses more on tool implementations and the application of logic to real systems, programs, and programming languages. Below, we outline our expertise in three focus areas.
This focus area studies a group of formal languages that is often used in both automatic and human-guided theorem provers, and forms the theoretical foundation of functional programming languages. We develop methods to verify properties of such systems, and tools to apply these methods fully automatically. In particular, we consider the study of termination (given an algorithm specified as a higher-order term rewriting system, and given any input, will it eventually produce an output?), complexity (how quickly will it produce such an output?), and equivalence (will it produce the same output as another system executed on the same input?)
This focus area is centered around scaling up program verification techniques to challenging programming paradigms such as fine-grained/lock-free concurrency, message-passing concurrency, higher-order functions, modules, and substructural/linear types. We develop semantics of programming languages such as C, Rust, and Scala, and use these semantics to verify properties such as type safety, functional correctness, deadlock freedom, non-interference, and compiler correctness. A key ingredient in this focus area is the use of program logics, in particular concurrent separation logic, to reason about programs at a suitable level of abstraction.
We implement and verify most of our techniques and theory in the Coq proof assistant using the Iris framework for higher-order concurrent separation logic. We study both interactive (human-guided) and mostly-automated techniques.
This focus area considers the verification of systems whose behavior is uncertain, e.g., due to the effects of sensors in the system. Examples for verification questions we ask are what is the probability that the system reaches an error state? and what is the expected time until we deplete our battery?. We assume that models are given in a high-level representation of a Markov decision process and study various extensions of Markov decision processes. Most techniques we develop are implemented in the probabilistic model checker Storm.