Distinguished Lecture Series
Overview:
"Machines Reasoning about Machines" |
|
"Learning to Think about the World" |
|
"Redoing the foundations of decision theory: Decision theory with subjective states and outcomes" |
|
"Value-based Software Engineering" |
Friday, October 26th, 2007 at 5:30pm
Lexmark Room, Main Building [info]
"Machines Reasoning about Machines"
J Strother Moore
Department of Computer Sciences
University of Texas at Austin
Abstract:
Computer hardware and software can be modeled precisely in mathematical logic. If expressed appropriately, these models can be executable. This allows them to be used as simulation engines or rapid prototypes. But because they are formal they can be manipulated by symbolic means: theorems can be proved about them, directly, with mechanical theorem provers. But how practical is this vision of machines reasoning about machines? In this highly personal talk, I will describe the 36 year history of the ``Boyer-Moore Project'' and discuss progress toward making formal verification practical. Among other examples I will describe important theorems about commercial microprocessor designs, including parts of processors by AMD, Motorola, IBM, Rockwell-Collins and others. Some of these microprocessor models execute at 90% the speed of C models and have had important functional properties verified. In addition, I will describe a model of the Java Virtual Machine, including class loading and bytecode verification and the proofs of theorems about JVM methods.
Biography:
J Strother Moore holds the Admiral B.R. Inman Centennial Chair in Computing Theory at the University of Texas at Austin. He is also chair of the department. He is the author of many books and papers on automated theorem proving and mechanical verification of computing systems. Along with Boyer he is a co-author of the Boyer-Moore theorem prover and the Boyer-Moore fast string searching algorithm. With Matt Kaufmann he is the co-author of the ACL2 theorem prover. Moore got his PhD from the University of Edinburgh in 1973 and his BS from MIT in 1970. Moore was a founder of Computational Logic, Inc., and served as its chief scientist for ten years. He and Bob Boyer were awarded the 1991 Current Prize in Automatic Theorem Proving by the American Mathematical Society. In 1999 they were awarded the Herbrand Award for their work in automatic theorem proving. Moore is a Fellow of both the American Association for Artificial Intelligence and the ACM and is a member of the NAE. Boyer, Moore, and Kaufmann were awarded the 2005 ACM Software Systems Award for the Boyer-Moore theorem prover.
November 8th, 2007
Lexmark Room, Main Building [info]
"Learning to Think about the World"
Leslie Pack Kaelbling
Computer Science and Artificial Intelligence Laboratory (CSAIL)
Massachusetts Institute of Technology
Abstract:
In the last 10 years, the combination of techniques from machine learning, statistics, and operations research has allowed major advances in learning and planning for uncertain environments. Reasonably large problems can be solved using current techniques. But what if we want to scale up to the uncertain learning and planning problem that you face every day? It is many orders of magnitude larger than the biggest problem we can solve currently.
In this talk, I'll describe three pieces of work that try to begin to
address learning and reasoning in truly huge environments. The first
is a method for learning probabilistic rules to describe naive
physics models of the interactions between objects. The second is a
logical particle filtering method that allows probabilistic state
estimation to be carried out in domains with very large or unbounded
numbers of individuals. The last is a planning algorithm that tries
to find a small planning problem instance within a large domain
description, in order to speed up planning for apparently simple
problems in very large domains.
January 15th, 2008 at
5:30
Auditorium at Young Library[info]
"Redoing the foundations of decision theory:
Decision theory with subjective states and outcomes"
Joe Halpern
Cornell University
Abstract:
The standard approach in decision theory (going back to Savage) is to place a preference order on acts, where an act is a function from states to outcomes. If the preference order satisfies appropriate postulates, then the decision maker can be viewed as acting as if he has a probability on states and a utility function on outcomes, and is maximizing expected utility. This framework implicitly assumes that the decision maker knows what the states and outcomes are. That isn't reasonable in a complex situation. For example, in trying to decide whether or not to attack Iraq, what are the states and what are the outcomes? We redo Savage viewing acts essentially as syntactic programs. We don't need to assume either states or outcomes. However, among other things, we can get representation theorems in the spirit of Savage's theorems; for Savage, the agent's probability and utility are subjective; for us, in addition to the probability and utility being subjective, so is the state space and the outcome space. I discuss the benefits, both conceptual and pragmatic, of this approach. As I show, among other things, it provides an elegant solution to framing problems.
This is joint work with Larry Blume and David Easley. No prior
knowledge of Savage's work is assumed.
Biography:
Joseph Y. Halpern received a B.Sc. in mathematics from the University of Toronto in 1975 and a Ph.D. in mathematics from Harvard in 1981. In between, he spent two years as the head of the Mathematics Department at Bawku Secondary School, in Ghana. He is currently a professor of computer science at Cornell University, where he moved in 1996 after spending 14 years at the IBM Almaden Research Center. His interests include reasoning about knowledge and uncertainty, decision theory and game theory, fault-tolerant distributed computing, causality, and security. Together with his former student, Yoram Moses, he pioneered the approach of applying reasoning about knowledge to analyzing distributed protocols and multi-agent systems; he won a Godel Prize for this work. He received the Publishers' Prize for Best Paper at at the International Joint Conference on Artificial Intelligence in 1985 (joint with Ronald Fagin) and in 1989, and the Reiter Prize for best paper at the Conference on Knowledge Representation and Reasoning in 2006 (joint with Larry Blume and David Easley). He has coauthored 6 patents, two books ("Reasoning About Knowledge" and "Reasoning About Uncertainty"), over 100 journal publications, and over 150 conference publications. He is a former editor-in-chief of the Journal of the ACM, a Fellow of the ACM, the AAAI, and the AAAS, and was the recipient of a Guggenheim and a Fulbright Fellowship.
April 7th, 2008 at 5:30
Auditorium at Young Library[info]
"Value-based Software Engineering"
Barry Boehm
University of Southern California
Abstract:
Much of current software engineering practice and research is done in a value-neutral setting, in which every requirement, use case, object, test case, and defect is equally important. However most studies of the critical success factors distinguishing successful from failed software projects find that the primary critical success factors lie in the value domain.
The value-based software engineering (VBSE) agenda discussed in this
chapter and exemplified in the other chapters involves integrating value
considerations into the full range of existing and emerging software
engineering principles and practices. The chapter then summarizes the
primary components of the agenda: value-based requirements engineering,
architecting, design and development, verification and validation,
planning and control, risk management, quality management, people
management, and an underlying theory of VBSE. It concludes with a global
roadmap for realizing the benefits of VBSE.
Biography:
Barry Boehm is the TRW Professor of Software Engineering and Director of the Center for Software Engineering at USC. His current research interests include software process modeling, software requirements engineering, software architectures, software metrics and cost models, software engineering environments, and value-based software engineering. His contributions to the field include the Constructive Cost Model (COCOMO), the Spiral Model of the software process, and the Theory W (win-win) approach to software management and requirements determination. He is a Fellow of the primary professional societies in computing (ACM), aerospace (AIAA), electronics (IEEE), and systems engineering (INCOSE), and a member of the US National Academy of Engineering.