Computer Laboratory

Technical reports

Branching-time reasoning for programs
(extended version)

Byron Cook, Eric Koskinen, Moshe Vardi

July 2011, 38 pages

Abstract

We describe a reduction from temporal property verification to a program analysis problem. Our reduction is an encoding which, with the use of procedures and nondeterminism, enables existing interprocedural program analysis tools to naturally perform the reasoning necessary for proving temporal properties (eg. backtracking, eventuality checking, tree counterexamples for branching-time properties, abstraction refinement, etc.). Our reduction is state-based in nature but also forms the basis of an efficient algorithm for verifying trace-based properties, when combined with an iterative symbolic determinization technique, due to Cook and Koskinen.

In this extended version, we formalize our encoding as a guarded transition system G, parameterized by a finite set of ranking functions and the temporal logic property. We establish soundness between a safety property of G and the validity of a branching time temporal logic property ∀CTL. ∀CTL is a sufficient logic for proving properties written in the trace-based Linear Temporal Logic via the iterative algorithm.

Finally using examples drawn from the PostgreSQL database server, Apache web server, and Windows OS kernel, we demonstrate the practical viability of our work.

Full text

PDF (0.9 MB)

BibTeX record

@TechReport{UCAM-CL-TR-788,
  author =	 {Cook, Byron and Koskinen, Eric and Vardi, Moshe},
  title = 	 {{Branching-time reasoning for programs (extended version)}},
  year = 	 2011,
  month = 	 jul,
  url = 	 {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-788.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-788}
}