INFORMATIKKOLLOQUIUM: 08.04.2002 17h00 E. Clarke: Grand Challenge:

From: Helmut Veith (kgs-owner@dbai.tuwien.ac.at)
Date: Fri Apr 05 2002 - 15:29:49 MEST

  • Next message: Helmut Veith: "A. Avron: Transitive Closure and Inductive Reasoning"

    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.



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