Invited talks

Among the highlights of our program are three invited talks.

• Sir Charles Antony Richard Hoare, FRS, FREng, FBCS, Microsoft Research
  • ACM SIGPLAN Programming Languages Achievement Award Interview
    [Show details]

    Abstract: To come soon!

    

    Bio of Sir Hoare: Sir C. A. R. Hoare's interest in computing was awakened in the early fifties, when he studied philosophy (together with Latin and Greek) at Oxford University, under the tutelage of John Lucas. He was fascinated by the power of mathematical logic as an explanation of the apparent certainty of mathematical truth. During his National Service (1956-1958), he studied Russian in the Royal Navy. Then he took a qualification in statistics (and incidentally) a course in programming given by Leslie Fox). In 1959, as a graduate student at Moscow State University, he studied the machine translation of languages (together with probability theory, in the school of Kolmogorov). To assist in efficient look-up of words in a dictionary, he discovered the well-known sorting algorithm Quicksort.

    On return to England in 1960, he worked as a programmer for Elliott Brothers, a small scientific computer manufacturer. He led a team (including his later wife Jill) in the design and delivery of the first commercial compiler for the programming language Algol 60. He attributes the success of the project to the use of Algol itself as the design language for the compiler, although the implementation used decimal machine code. Promoted to the rank of Chief Engineer, he then led a larger team on a disastrous project to implement an operating system. After managing a recovery from the failure, he moved as Chief Scientist to the computing research division, where he worked on the hardware and software architecture for future machines.

    These machines were cancelled when the Company merged with its rivals, and in 1968 Tony took a chance to apply for the Professorship of Computing Science at the Queen's University, Belfast. His research goal was to understand why operating systems were so much more difficult than compilers, and to see if advances in programming theory and languages could help with the problems of concurrency. In spite of civil disturbances, he built up a strong teaching and research department, and published a series of papers on the use of assertions to prove correctness of computer programs. He knew that this was long term research, unlikely to achieve industrial application within the span of his academic career.

    In 1977 he moved to Oxford University, and undertook to build up the Programming Research Group, founded by Christopher Strachey. With the aid of external funding from government initiatives, industrial collaborations, and charitable donations, Oxford now teaches a range of degree courses in Computer Science, including an external Master's degree for software engineers from industry. The research of his teams at Oxford pursued an ideal that takes provable correctness as the driving force for the accurate specification, design and development of computing systems, both critical and non-critical. Well-known results of the research include the Z specification language, and the CSP concurrent programming model. A recent personal research goal has been the unification of of a diverse range of theories applying to different programming languages, paradigms, and implementation technologies.

    Throughout more than thirty years as an academic, Tony has maintained strong contacts with industry, through consultancy, teaching, and collaborative research projects. He took a particular interest in the sustenance of legacy code, where assertions are now playing a vital role, not for his original purpose of program proof, but rather in instrumentation of code for testing purposes. On reaching retirement age at Oxford, he welcomed an opportunity to go back to industry as a senior researcher with Microsoft Research in Cambridge. He hopes to expand the opportunities for industrial application of good academic research, and to encourage academic researchers to continue the pursuit of deep and interesting questions in areas of long-term interest to the software industry and its customers.

• J. Strother Moore, University of Texas at Austin
  • Meta-Level Features in an Industrial-Strength Theorem Prover
    [Show details]

    Abstract: The ACL2 theorem prover -- the current incarnation of "the" Boyer-Moore theorem prover -- is a theorem prover for an extension of a first-order, applicative subset of Common Lisp. The ACL2 system is coded in that same language, which makes possible several powerful meta-level and reflexive features. After establishing that ACL2 is actually in use at several major microprocessor manufacturers to verify functional correctness of important components of commercial designs, I will discuss some of the consequences of ACL2's design.

    Among the applications of ACL2 are the following:

    • All elementary floating point operations on all desktop AMD microprocessors fabricated since 1997 have been verified with ACL2 to satisfy the IEEE 754 floating point standard.

    • The Rockwell Collins AAMP7 cryptoprocessor was verified with ACL2 as specified by the EAL-7 level of the Common Criteria and was certified capable of simultaneously processing unclassified through Top Secret Codeword classified data.

    • The media unit of the Centaur (VIA) Nano 64-bit x86 CPU has been verified to be functionally correct with ACL2. In addition, important properties of the clock tree for the entire x86 design have been verified.

    These and other industrial applications establish that the ACL2 system provides a useful specification and modeling language as well as a useful mechanical theorem proving environment.

    Surprising to many in the programming languages community is the fact the ACL2 language is remarkably primitive: it is untyped, all functions are total, and there are no functional objects (it is a first-order language). These compromises can make ACL2 models more verbose and cumbersome than comparable models in other languages would be, but also make it easier to build a powerful proof engine for the language. The presence of a powerful theorem prover can in turn be exploited to produce very efficient runtime code.

    The ACL2 theorem prover is a program written in the same language supported by the theorem prover. All of the data structures used in the theorem prover are objects in that language. Users of the proof assistant must understand the language since it is their specification and modeling language. Furthermore, users are permitted to write ``programs'' (i.e., to define functions) in the language and to run those programs on the theorem prover's data because those programs are side-effect-free. Thus, the prover can be opened up to much user-specialization.

    Among other things, the ACL2 user can

    1. build and efficiently run models of complex computing artifacts like microprocessors or floating point units, while experimenting with specifications, theorems, and proofs;

    2. build new theorem prover components, use ACL2 to prove that those components meet the specifications required by ACL2, and then cause the system to use the user-defined components in place of the primitives provided by the ACL2 implementors; and

    3. define functions that inspect the goal being proved and the ACL2 data base and context and then compute goal-specific hints at runtime.

    Perhaps surprisingly, such sophisticated meta-level facilities were implemented primarily at the requests of the ACL2 user community and find routine use in the industrial-scale projects mentioned above. ACL2 is thus exploiting the programming prowess of the engineers and scientists who use it to produce industrial-scale proofs.

    Finally, I will briefly note some of the omissions from ACL2 language including the lack of quantifiers, syntactic typing, and higher order features. The power of the automatic theorem prover mitigates these omissions.

    Bio: J Strother Moore holds the Admiral B.R. Inman Centennial Chair in Computing Theory in the Department of Computer Science at the University of Texas at Austin. He was chair of the Computer Science Department for 8 years, 2001-09, and led the $120M drive to build the Bill and Melinda Gates Center for Computer Science and the Michael and Susan Dell Computer Science Hall, upon which ground was broken in October, 2010. 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 S.B. in mathematics from MIT in 1970 and his Ph.D. in computational logic from the University of Edinburgh in 1973. Moore was a co-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 the American Association for Artificial Intelligence, an ACM Fellow, and a member of the National Academy of Engineering (NAE). Boyer, Moore, and Kaufmann won the 2005 ACM Software System Award "For pioneering and engineering a most effective theorem prover (named the Boyer-Moore Theorem Prover) as a formal methods tool for verifying safety-critical hardware and software."

• Jennifer Rexford, Princeton University
  • Programming Languages for Programmable Networks
    [Show details]

    Abstract: To come soon!

    Bio: Jennifer Rexford is a Professor in the Computer Science department at Princeton University. From 1996-2004, she was a member of the Network Management and Performance department at AT&T Labs--Research. Jennifer is co-author of the book "Web Protocols and Practice" (Addison-Wesley, May 2001). She served as the chair of ACM SIGCOMM from 2003 to 2007. Jennifer received her BSE degree in electrical engineering from Princeton University in 1991, and her MSE and PhD degrees in computer science and electrical engineering from the University of Michigan in 1993 and 1996, respectively. She was the 2004 winner of ACM's Grace Murray Hopper Award for outstanding young computer professional.