Press Information
The inaugural ceremony for the KIT Focus COMMputation has taken place on
- 12 November 2009 at 4 pm
- in Tulla auditorium (map), Karlsruhe Institute of Technology (KIT).
Program
Prof. Dr. Norbert Henze, KIT-Board Member and Chief Information Officer
Opening speach
Prof. Dr. Heinz Wörn, Dean of the Department of Computer Science
Opening speach
Prof. Dr. Hartmut Schmeck, Scientific Spokesperson of the KIT-Focus COMMputation
"COMMputation = COMMunication + COMputation"
Prof. Dr. Prabhakar Raghavan, Head of Yahoo! Labs
"Heavy Tails and Models for the Web and Social Networks"
Prof. Dr. Edmund Clarke, FORE Systems University Professor of Computer Science and Professor of Electrical and Computer Engineering, Carnegie-Mellon University, Pittsburgh PA
"Model Checking. My 28-year Quest to Overcome the State Explosion Problem"
18.00 Uhr: Reception
First keynote talk by Prabhakar Raghavan (Yahoo! Research):
"Heavy Tails and Models for the Web and Social Networks"
Abstract. The literature is rich with (re)discoveries of power law phenomena; this is especially true of observations of link and traffic behavior on the Web. We survey the origins of these phenomena and several (yet incomplete) attempts to model them, including our recent work on the compressibility of the Web graph and social networks. We argue that social networks exhibit characteristics that are very different from the Web, then present a number of open problems arising from these observations.
Biography. Prabhakar Raghavan is the head of Yahoo! Labs. Raghavan's research interests include text and web mining, and algorithm design. He is a consulting professor of Computer Science at Stanford University and editor-in-chief of the Journal of the ACM. He has co-authored two textbooks, on randomized algorithms and on information retrieval. Raghavan received his PhD from Berkeley and is a member of the National Academy of Engineering and a fellow of the ACM and of the IEEE. Prior to joining Yahoo!, he was the chief technology officer at Verity and has held a number of technical and managerial positions at IBM Research.
Second keynote talk by Edmund Clarke (CMU):
"Model Checking. My 28-year Quest to Overcome the State Explosion Problem"
Abstract. Model Checking is an automatic verification technique for state-transition systems that are finite-state or that have finite-state abstractions. In the early 1980’s in a series of joint papers with my graduate students E.A. Emerson and A.P. Sistla, we proposed that Model Checking could be used for verifying concurrent systems and gave algorithms for this purpose. At roughly the same time, Joseph Sifakis and his student J.P. Queille at the University of Grenoble independently developed a similar technique. Model Checking has been used successfully to reason about computer hardware and communication protocols and is beginning to be used for verifying computer software. Specifications are written in temporal logic, which is particularly valuable for expressing concurrency properties. An intelligent, exhaustive search is used to determine if the specification is true or not. If the specification is not true, the Model Checker will produce a counterexample execution trace that shows why the specification does not hold. This feature is extremely useful for finding obscure errors in complex systems. The main disadvantage of Model Checking is the state-explosion problem, which can occur if the system under verification has many processes or complex data structures. Although the state-explosion problem is inevitable in worst case, over the past 27 years considerable progress has been made on the problem for certain classes of state-transition systems that occur often in practice. In this talk, I will describe what Model Checking is, how it works, and the main techniques that have been developed for combating the state explosion problem.
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. He was named a University Professor in 2008.
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 verification 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, Logic and Computation, and IEEE Transactions in Software Engineering. He is the former editor-in-chief of Formal Methods in Systems Design. He is on the organizing committee of Logic in Computer Science (LICS) and on the steering committee of Computer-Aided Verification (CAV). He received a Technical Excellence Award from the Semiconductor Research Corporation in 1995. He was a co-winner with Randy Bryant, Allen Emerson, and Kenneth McMillan of the ACM Kanellakis Award in 1998 for the development of Symbolic Model Checking. In 1999 he received an Allen Newell Award for Excellence in Research from the Carnegie Mellon Computer Science Department. In 2004 he received the IEEE Harry H. Goode Memorial Award for significant and pioneering contributions to formal verification of hardware and software systems, and for the profound impact these contributions have had on the electronics industry. He was elected to the National Academy of Engineering in 2005 for contributions to the formal verification of hardware and software correctness. He was a recipient with Allen Emerson and Joseph Sifakis of the 2007 ACM Turing Award for his role in developing Model Checking into a highly effective verification technology, widely adopted in the hardware and software industries. In 2008 he received the CADE Herbrand Award for Distinguished Contributions to Automated Reasoning in recognition of his role in the invention of Model Checking and his sustained leadership in the area for more than two decades. Dr. Clarke is a Fellow of the ACM and the IEEE, and a member of Sigma Xi and Phi Beta Kappa.