We are honored to announce the following invited speakers at SAT'12:
More details are given below. The presence of both speakers has been confirmed, although the titles and the abstracts of the talks may be provisional.
Speaker: Aaron Bradley
Title: SAT-based Verification with IC3: Foundations and Demands
The recently introduced model checking algorithm, IC3, has quickly proven to be among the best SAT-based safety model checkers. Many implementations now exist. Unlike its predecessors --- BMC, k-induction, and the interpolant-based approach (ITP) --- IC3 does not unroll the transition relation. Instead, it relies on generating small "relatively inductive" lemmas incrementally until a sufficient set has been found to imply the inductiveness of the given safety property, or until the lemmas have guided the search to a counterexample trace. Consequently, the queries that IC3 poses to the SAT solver differ significantly in character from those posed by its predecessors. In this talk, I will provide background on IC3 and then focus on the demands that IC3 makes of the SAT solver.
In particular, in contrast to the few hard queries that BMC, k-induction, and ITP pose, IC3 poses hundreds to thousands of incremental queries per second. Furthermore, IC3 benefits from unsatisfiable cores restricted to assumptions as well as "lifted" partial assignments. Hence, IC3 requires a sophisticated yet efficient incremental solver. Additionally, IC3's incremental nature makes parallelization easy and motivates a new form of parallel SAT solver: one in which multiple threads can pose incremental queries over a common growing core of constraints. The FAIR algorithm, which extends IC3 to all of LTL, poses even more challenges to an incremental solver. Finally, extending IC3 to word-level analysis makes similar demands of the SMT solver.
Aaron Bradley earned a Ph.D. from Stanford under the supervision of Zohar Manna, with whom he co-authored the book "The Calculus of Computation: Decision Procedures with Applications to Verification." He is currently adjunct professor in the ECEE department at the University of Colorado, Boulder.
Aaron Bradley recently developed IC3, an algorithm for formal verification that leverages SAT technology to achieve impressive efficiency -- it is considered nowadays one of the most stable and effective verification algorithms for the verification of sequential hardware designs. Interestingly, IC3 uses SAT technology in several non-standard and intellectually challenging ways. This, combined with the fast adoption of IC3 in industrial settings, may influence the future of SAT research.
Speaker: Donald Knuth
Title: Satisfiability and The Art of Computer Programming
The speaker will describe his adventures during the past eight months when he has been intensively studying as many aspects of SAT solvers as possible, in the course of preparing about 100 pages of new material for Volume 4B of The Art of Computer Programming.
Donald E. Knuth (B.S. and M.S., Case Institute of Technology 1960; Ph.D., California Institute of Technology 1963) is Professor Emeritus of The Art of Computer Programming at Stanford University, where he supervised the Ph.D. dissertations of 28 students since becoming a professor in 1968. He is the author of numerous books, including four volumes (so far) of The Art of Computer Programming, five volumes of Computers & Typesetting, nine volumes of collected papers, and a non-technical book entitled 3:16 Bible Texts Illuminated. His software systems TeX and MF are extensively used for book publishing throughout the world.
He is a member of the American Academy of Arts and Sciences, the National Academy of Sciences, and the National Academy of Engineering, and he is a foreign associate of the French, Norwegian, Bavarian, and Russian science academies as well as the Royal Society of London. He received the Turing Award from the Association for Computing Machinery in 1974; the National Medal of Science from President Carter in 1979; the Steele Prize from the American Mathematical Society in 1986; the Adelskold Medal from the Royal Swedish Academy of Sciences in 1994; the Harvey Prize from the Technion of Israel in 1995; the John von Neumann Medal from the Institute of Electrical and Electronic Engineers in 1995; the Kyoto Prize from the Inamori Foundation in 1996; the Frontiers of Knowledge award from the BBVA Foundation in 2010; and the Faraday Medal from the IET in 2011. He holds honorary doctorates from Oxford University, the University of Paris, the Royal Institute of Technology in Stockholm, the University of St. Petersburg, the University of Marne-la-Vallee, Masaryk University, St. Andrews University, Athens University of Economics and Business, the University of Macedonia in Thessaloniki, the University of Tubingen, the University of Oslo, the University of Antwerp, the Swiss Federal Institute of Technology in Zurich, the University of Bordeaux, the University of Glasgow, and nineteen colleges and universities in America.