[Acpc-l] INFORMATIKKOLLOQUIUM: 08.04.2002 17h00 E. Clarke: Grand Challenge: Model Checking Software

[Therese Schwarz]

Der Fachbereich Informatik und die Österreichische Computergesellschaft
laden zu folgendem Vortrag ein:
*************************************************************************************
Grand Challenge: Model Checking Software
Professor Edmund E. Clarke
FORE Systems Professor of Computer Science
Department of Computer Science
Carnegie Mellon University

Zeit: 8. April 2002, 17:00 c.t.
Ort: Zemanek Hörsaal, Favoritenstraße 9-11/Erdgeschoß, roter Bereich

Abstract:
Model Checking is a technique for verifying finite-state concurrent systems
such as sequential circuit designs and communication protocols. It has a
number of advantages over traditional approaches that are based on simulation,
testing, and deductive reasoning. In particular, model checking is automatic
and usually quite fast. Also, if the design contains an error, model checking
will produce a counterexample that can be used to pinpoint the source of the
error. The method has been used successfully in practice to verify real 
industrial
designs, and companies are beginning to market commercial model checkers.
The main challenge in model checking is dealing with the state space explosion
problem. This problem occurs in systems with many components that can interact
with each other or systems with data structures that can assume many different
values. In such cases the number of global states can be enormous. Researchers
have made considerable progress on this problem over the last ten years. In 
this
talk I will survey the progress that has been made, give examples of what 
model
checking is capable of doing now, and pose some directions for future 
research.
In particular, I will speculate on how to solve the biggest challenge in 
model checking:
Software verification.

Biography:
Edmund M. Clarke received a B.A. degree in mathematics from the University of
Virginia, Charlottesville, VA, in 1967, an M.A. degree in mathematics from 
Duke
University, Durham NC, in 1968, and a Ph.D. degree in Computer Science from
Cornell University, Ithaca NY, in 1976.

After receiving his Ph.D., he taught in the Department of Computer Science, 
Duke
University, for two years. In 1978 he moved to Harvard University, 
Cambridge, MA
where he was an Assistant Professor of Computer Science in the Division of 
Applied
Sciences. He left Harvard in 1982 to join the faculty in the Computer Science
Department at Carnegie-Mellon University, Pittsburgh, PA. He was appointed 
Full
Professor in 1989. In 1995 he became the first recipient of the FORE 
Systems Professorship,
an endowed chair in the School of Computer Science.

Dr. Clarke's interests include software and hardware verification and 
automatic
theorem proving. In his Ph.D. thesis he proved that certain programming 
language
control structures did not have good Hoare style proof systems. In 1981 he and
his Ph.D. student Allen Emerson first proposed the use of Model Checking as a
erification technique for finite state concurrent systems. His research 
group pioneered
the use of Model Checking for hardware verification. Symbolic Model Checking
using BDDs was also developed by his group. This important technique was the
subject of Kenneth McMillan's Ph.D. thesis, which received an ACM Doctoral
Dissertation Award. In addition, his research group developed the first 
parallel
resolution theorem prover (Parthenon) and the first theorem prover to be based
on a symbolic computation system (Analytica).

Dr. Clarke has served on the editorial boards of Distributed Computing and 
Logic
and Computation. He is currently on the editorial board of IEEE 
Transactions in
Software Engineering and is editor-in-chief of Formal Methods in Systems 
Design.
He is on the steering committees of two international conferences, Logic in 
Computer
Science and Computer-Aided Verification. He was a cowinner along with Randy
Bryant, Allen Emerson, and Kenneth McMillan of the ACM Kanellakis Award in 
1999
for the development of Symbolic Model Checking. For this work he also 
received a
Technical Excellence Award from the Semiconductor Research Corporation in 1995
and an Allen Newell Award for Excellence in Research from the Carnegie Mellon
Computer Science Department in 1999. Dr. Clarke is a Fellow of the 
Association for
Computing Machinery, a member of the IEEE Computer Society, Sigma Xi, and 
Phi Beta Kappa.