[Acpc-l] INFORMATIKKOLLOQUIUM: 08.04.2002 17h00 E. Clarke: Grand
Challenge: Model Checking Software
Therese Schwarz
sek@dbai.tuwien.ac.at
Wed, 03 Apr 2002 13:10:56 +0200
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
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.
*************************************************************************
Der Fachbereich Informatik wird unterstützt von : SIEMENS AG