[Pl-seminar] Semantics Seminar Schedule

[Mitchell Wand]

NU Programming Languages Seminar
Wednesday, 12/13/06
11:45am-1:30pm
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Pete Maniolos
Georgia Tech

A Complete Compositional Reasoning Framework with Applications to
Hardware Verification

Abstract:
We present a complete compositional reasoning framework for
verifying that a concrete system satisfies the same safety and
liveness properties as its specification. Our framework consists
of a powerful theory of refinement and a set of convenient,
easily-applicable, and complete compositional proof rules. An
important benefit of our approach over current methods is that
the counterexamples generated tend to be much simpler, as bugs
are isolated to a particular step in the composition proof.

We have applied our work to the problem of hardware
verification. This is one of the major challenges currently
facing the hardware industry, with recent estimates indicating
that verification accounts for up to 70% of the total development
costs for new products. We show that our framework greatly
extends the applicability of decision procedures by automatically
proving that complex pipelined machines defined at the RTL level
and containing features such as out-of-order completion, branch
prediction, caches, and deep pipelines refine their instruction
set architectures.

This is joint work with Sudarshan Srinivasan.

Speaker Bio: 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. 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.

Pete's primary research interest is formal verification. This
includes developing algorithms, methodologies, concepts, and
tools to formally and mechanically reason about both software and
hardware systems. Pete is particularly interested in decision
procedures, theorem proving, model checking, refinement, and
abstraction. He also has broad interests in systems, software
engineering, logic, computational biology, distributed computing,
and pedagogy.



Upcoming Events:

# Wed 1/24 Bil Lewis, Omniscient Debugging


--Mitch