Abstract: I will present a compositional theory of refinement for the branching time framework and will show how to apply it to automatically verify both safety and liveness properties of pipelined machines using UCLID.

The existence of refinement maps in the linear time framework was studied in an influential paper by Abadi and Lamport, who showed that under certain conditions, e.g., machine closure, finite invisible nondeterminism, internal continuity, the use of history and prophecy variables, etc., refinement maps exist. I will present a similar result for the branching time framework that does not depend on any of the above conditions. A consequence is that refinement maps always exist in the linear time framework, subject only to the use of prophecy-like variables.

In the second part of the talk I will present an interesting application of the above results, based on joint work with Sudarshan K. Srinivasan. I will show how one can automatically prove that an instruction set architecture model satisfies the same safety and liveness properties as pipelined machine models containing features such as out-of-order completion, precise exceptions, branch prediction, and interrupts. Using UCLID and the SAT solver Siege, verification times for our approach are about 5% longer than verification times for the typical Burch and Dill type proofs.

Biography: Panagiotis (Pete) Manolios is an Assistant Professor in the College of Computing at the Georgia Institute of Technology. He is also an Adjunct Assistant Professor in the School of Electrical and Computer Engineering and a member of CERCS, the Center for Experimental Research in Computer Systems. He has a B.S. and an M.A. in Computer Science from Brooklyn College and a Ph.D. in Computer Sciences from the University of Texas at Austin (2001), under the supervision of J Strother Moore. Pete's primary research interest is the formal verification of computing systems. This includes developing algorithms, methodologies, concepts, and tools to formally and mechanically reason about both software and hardware systems. Pete is particularly interested in theorem proving, model checking, and abstraction. He also has broad interests in distributed computing, systems, algorithms, logic, programming languages, software engineering, security, the theory of computation, set theory, the foundations of mathematics, and pedagogy.