Keynote Speakers

Toward Automated Software Development

Doug Smith

Doug Smith

Kestrel Institute
http://www.kestrel.edu/home/people/smith/

Abstract

The ASE conference series is rooted in the 1981 Knowledge-Based Software Assistant (KBSA) document and the ensuing US Air Force Rome Labs research program. KBSA addressed automated tool support for the entire software lifecycle, including project management, requirements, specifications, code generation, and evolution. A core goal of KBSA and ASE is the automated generation of code from requirement-level specifications, which promises benefits in three directions: (1) High Assurance - generation of correct code, as well as certification information as a by-product, (2) Productivity through automation, and (3) high Performance through machine application of best-practice design knowledge. Benefits should also include lowering of the cost of lifecycle ownership, due to automated treatment of evolving requirements. This talk will briefly review the KBSA vision, as well as a personal view of developments in the past decade.

Biography

Dr. Douglas R. Smith is Principal Scientist at Kestrel Institute. He is also is Executive Vice-President and Chief Technology Officer of Kestrel Technology LLC. He is a Fellow of the American Association of Artificial Intelligence (AAAI) and an ASE Fellow (Automated Software Engineering). He taught an advanced graduate course on knowledge-based software development at Stanford University during 1986-2000. Dr. Smith was Chairman of IFIP Working Group 2.1 on Algorithmic Languages and Calculi from 1994-2000.

His main research interest has been mechanizing the development of software from formal specifications. He is mainly responsible for the development of KIDS (Kestrel Interactive Development System), which has been used to synthesize many algorithms, including a variety of complex high-performance scheduling applications for the US Air Force.

Theoretical developments arising from experience with KIDS were a key motivation for building the Specware, Designware, and Planware systems. His current research focuses on automating system design, including the automatic enforcement of cross-cutting safety and security policies, and system code generation from formalized design patterns and software architectures. A brief discussion of the intellectual roots of Kestrel's research may be found here.

Dr. Smith has over 30 years experience in the field of automated program synthesis and has published over 75 papers (see the CiteSeer surveys of most cited papers in Software Engineering and most cited authors in Computer Science). He has one patent and one patent pending. He received the Ph.D. in Computer Science from Duke University in 1979.


Specifying and Verifying Software

Rustan Leino

K. Rustan M. Leino

Microsoft Research, Redmond
http://research.microsoft.com/~leino/

Abstract

Software verification presents many challenges. One of these is providing programmers with automated tool support for verification, another is providing specification support that captures common programming idioms. In this talk, I will discuss these two challenges, drawing from experience with building program verifiers for Spec# and C. I will also give a demo of the Spec# programming system, which includes an automatic static program verifier.

Biography

Rustan Leino is a Principal Researcher in the Programming Languages and Methods group at Microsoft Research, Redmond, where his research centers around programming tools. He currently leads the Spec# project, which explores enforceable contracts in object-oriented programming. He works on the design and implementation of the Spec# programming language as well as its static program verifier, called Boogie. He is also involved in a new project to verify C code, which reuses the Boogie tool. Before joining Microsoft Research, Leino worked as a researcher at DEC/Compaq SRC, where among other things he led the Extended Static Checking for Java (ESC/Java) project, a light-weight program checker built on the technology of program verification. His PhD thesis from Caltech (1995) addressed an important specification problem in ESC/Modula-3. Before going to graduate school, Leino worked as a software developer and technical lead in Windows/NT at Microsoft. He has written code that shipped in releases of Windows 3.0, Windows 3.1, and Windows/NT 3.5. In his spare time, he plays and records music, teaches step aerobics, and spends time with his wife and four children.


The Embarrassing Truth About Software and Automation and What Should be Done About It

Bran Selic

Bran Selic

IBM
http://www-306.ibm.com/software/rational/bios/selic.html

Abstract

Automation is the most successful technological means for achieving dramatic improvements in both productivity and quality. The displacement of manual manufacturing methods by automated processes is at the core of the Industrial Revolution and accounts for much of what we usually refer to "progress" over the past several centuries. The introduction of computers and computer software more than a half century ago create unprecedented opportunities in this regard: they can not only help us automate the physical processes involved in production but also many of the highly mechanistic and error-prone mental processes involved in design. The opportunity provided by software and computers in this regard is without precedent.

Yet, when one reviews the history of computer-based automation in the process of software design, we find that, following the invention of compilers almost fifty years ago, the use of computer-based automation has made little difference in the lives and methods of the vast majority of software developers. This is not due to lack of opportunity — software is an eminently flexible medium limited mostly by imagination — but mostly due to often unrecognized social and cultural factors.

In this talk, we first examine the history of the use of computer-based automation in software development and speculate on the reasons why the software development community has spurned the opportunities that it offers. Next, we identify the scope of opportunities offered by current computer-based technology and what could be done to exploit this potential to its fullest.

Biography

Bran Selic is a Distinguished Engineer at IBM Canada and an adjunct professor of computer science at Carleton University in Ottawa. At IBM he is a member of the CTO team, responsible for defining the strategic direction for Rational's software tool products. Bran has over 30 years of experience in designing and implementing large-scale industrial software systems and has pioneered the application of model-driven development methods in real-time applications. He is currently chair of the OMG team responsible for the UML 2 standard.

Bran received his Dipl.Ing degree in 1972 and his Mag.Ing degree in 1974, both from the University of Belgrade in Yugoslavia.