**Previous message:**kgs@logic.at: "Lecture Announcement: Jan Johannsen"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]

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.

**Next message:**Helmut Veith: "A. Avron: Transitive Closure and Inductive Reasoning"**Previous message:**kgs@logic.at: "Lecture Announcement: Jan Johannsen"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]

*
This archive was generated by hypermail 2b30
: Fri Apr 05 2002 - 15:31:12 MEST
*