[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...
URL: <http://cs-mailman.bu.edu/pipermail/cs-talks/attachments/20161116/ae3f8b00/attachment.html>

More information about the cs-talks mailing list