[cs-talks] Temporal Verification of Systems Code, TODAY 11/16 at 5pm, MCS B08
Harrington, Jacob Walter
jwharrin at bu.edu
Wed Nov 16 09:19:22 EST 2016
Temporal Verification of Systems Code
Eric Koskinen, Yale University
Wednesday November 16th, 2016 at 5pm in MCS B08
Abstract: Temporal logic properties permit programmers to specify sophisticated safety and liveness properties of systems. However, 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.
In this talk I will describe a series of recent works in which we have developed techniques for proving temporal properties of real systems code. First, I will discuss a novel reduction from temporal property verification to a program analysis problem [CAV'11]. In this work we produce an encoding which, through the use of recursion and nondeterminism, enables off-the-shelf program analysis tools to naturally perform the reasoning necessary for proving temporal properties (e.g. backtracking, eventuality checking, tree
counterexamples for branching-time properties, abstraction refinement, etc.). Next, I will briefly describe how our technique can be used to additionally reason about trace-based properties [POPL'11] as well as temporal properties with branching [PLDI'13]. The former uses an iterated symbolic partial determinization strategy while the latter is based on the observation that existential reasoning can be reduced to universal reasoning if the system's state-space is appropriately restricted.
With the above techniques we have proved temporal properties of a wide range of examples drawn from the PostgreSQL database server, Apache web server, and Windows OS kernel, thus demonstrating the practical viability of our work.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the cs-talks