Reasoning About Non-Determinism in Programs

Presented as part of the 2012 HCSS conference.

Abstract:

Modern software systems are ubiquitous and complex, often running on critical platforms ranging from human implant devices to nuclear power plant controls. How can we be sure that these programs will behave as intended? Programmers must first specify the correct behavior of their programs, and one widely accepted specification language is temporal logic. Despite decades of research in finite-state contexts and some adaptations of finite-state algorithms, we still lack scalable tools for proving temporal logic properties of software.

Temporal property languages that support both universal and existential temporal reasoning allow us to ask and answer sophisticated questions about the non-deterministic behavior of systems. For example, in the domain of planning, the temporal property A(EF(p W p)) is useful when trying to establish that the system could always terminate and will always establish p if and when it does terminate. A proof of this property can be used when searching for a plan for causing termination if and when it is desired. Similar applications arise in games, formal verification for security, as well as precondition/environment synthesis.

The problem is that, until now, reliable and scalable automatic methods for proving properties of this sort in the presence of (possibly infinite-state) programs have remained unknown. In this talk we will describe a technique for supporting existential reasoning for programs that is based on a reduction to known approaches for universal subsets. This novel method gives rise to a new class of automatic tools. Formally we add new sound and complete relational proof rules for CTL's existential operators (e.g. EF, EG, etc.) to the relational proof system for the universal subset of CTL from our previous work [CAV 2011 and FMSD 2012]. These new proof rules unify aspects common to the universal and existential subsets of CTL, while highlighting an additional requirement necessary for existential reasoning: recurrence sets [Ganty et al., POPL 2009]. An algorithm is then provided that uses counterexamples to failed proof attempts to find the recurrence sets that are necessary to prove the desired CTL property.

Using a preliminary implementation, we demonstrate the practical viability of the approach on examples drawn the PostgreSQL database server, the Apache web server, and the Windows OS kernel. We also demonstrate how proofs found in our system can be used in useful ways in given domains such as planning, security analysis, games, precondition/environment synthesis, etc.

Biography:

I am a research scientist at the Courant Institute of Mathematical Sciences at New York University. Previously I was a Ph.D student at the Univeristy of Cambridge (UK) Computer Laboratory, jointly supervised by Byron Cook and Mike Gordon. I am funded by the Gates Cambridge Scholarship. I received my Sc.M from Brown University, where I worked with Maurice Herlihy.

In my research, I develop new mathematical methods for making software safer and more efficient, and apply those methods to realistic computer systems. In recent years I have accomplished this in two ways. First, I have improved programming languages by introducing new language features which are, by design both safer and more efficient. In particular, I am concerned with language advances which enable engineers to safely produce software which consists of parallel computation (e.g. my work on Transactional Boosting and Coarse-Grained Transactions). Second, I have developed static and dynamic analysis techniques in order to better understand the performance (e.g. discovering symbolic complexity bounds), understand the behavior (e.g. request tracing in BorderPatrol), discover bugs and formally prove correctness of programs (e.g. proving Linear Temporal Logic properties via a reduction to a program analysis task and symbolic partial determinization).