Invited Speakers

SAT 2013 features three excellent invited speakers:

• Albert Atserias:
  The Proof-Search Problem between Bounded-Width Resolution and Bounded-Degree Semi-Algebraic Proofs
  
• Edmund M. Clarke:
  Turing's Computable Real Numbers and Why They Are Still Important Today
  
• Peter Stuckey:
  There Are No CNF problems

More details are provided below.

• Albert Atserias (UPC Barcelona, Spain):
  
  Talk title: The Proof-Search Problem between Bounded-Width Resolution and Bounded-Degree Semi-Algebraic Proofs
  
  Abstract: In recent years there has been some progress in our understanding of the proof-search problem for very low-depth proof systems, e.g. proof systems that manipulate formulas of very low complexity such as clauses (i.e. resolution), DNF-formulas (i.e. R(k) systems), or polynomial inequalities (i.e. semi-algebraic proof systems). In this talk I will overview this progress. I will start with bounded-width resolution, whose specialized proof-search algorithm is as easy as uninteresting, but whose proof-search problem is unintentionally solved by certain versions of conflict-driven clause-learning algorithms with restarts. I will continue with R(k) systems, whose proof-search problem turned out to hide the complexity of certain two-player games of interest in the area of systems synthesis and verification. And I will close with bounded-degree semi-algebraic proof systems, whose proof-search problem turned out to hide the complexity of linear systems of equations over finite fields, among other problems.
  
  Bio: Albert Atserias received an engineering degree in computer science in 1997 from the Universitat Politècnica de Catalunya (UPC), a M.Sc. in computer science from the University of California at Santa Cruz (UCSC) in 1999, a Ph.D. in computer science from UPC in 2002, and a Ph.D. in computer science from UCSC also in 2002. Currently he is an Associate Professor at UPC where he has been teaching since 2002 to students in computer science and mathematics. In 2008, Dr. Atserias was a visiting scholar at the EECS department from the University of California at Berkeley.
  
  Dr. Atserias' research interests are in computational complexity, combinatorics, and applications of logic to computer science. More specifically, he has contributed to propositional proof complexity, descriptive complexity, and finite model theory. Dr. Atserias' work is known for building bridges between the two traditional tracks of theoretical computer science (track A and track B). Among his best known achievements is the connection he established between the two-player games for inexpressibility results in finite model theory and lower bound methods for propositional proof systems in proof complexity. In 2002 he received the Kleene Award for best student paper at the LICS conference for pioneering work in this area. More recent work of 2012 further connects the two-player games with lift-and-project methods in mathematical programming.
  
  
• Edmund M. Clarke (Carnegie Mellon University, USA):
  
  Talk title: Turing's Computable Real Numbers and Why They Are Still Important Today
  
  Abstract: Although every undergraduate in computer science learns about Turing Machines, it is not well known that they were originally proposed as a means of characterizing computable real numbers. For a long time, formal verification paid little attention to computational applications that involve the manipulation of continuous quantities, even though such applications are ubiquitous. In recent years, however, there has been great interest in safety-critical hybrid systems involving both discrete and continuous behaviors, including autonomous automotive and aerospace applications, medical devices of various sorts, control programs for electric power plants, and so on. As a result, the formal analysis of numerical computation can no longer be ignored. In this talk, we focus on one of the most successful verification techniques, temporal logic model checking. Current industrial model checkers do not scale to handle realistic hybrid systems. We believe that the key to handling more complex systems is to make better use of the theory of the computable reals, and computable analysis more generally. We argue that new formal methods for hybrid systems should combine existing discrete methods in model checking with new algorithms based on computable analysis. In particular we discuss a model checker we are currently developing along these lines.
  
  Bio: Edmund M. Clarke received a B.A. degree in mathematics from the University of Virginia in 1967, a M.A. degree in mathematics from Duke University in 1968, and a Ph.D. degree in computer science from Cornell in 1976. He taught at Duke University from 1976-1978 and at Harvard University from 1978-1982. Since 1982 he has been on the faculty in the Computer Science Department at Carnegie-Mellon University. 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 1981 he and a graduate 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 and software verification. In particular, his research group developed Symbolic Model Checking using BDDs, Bounded Model Checking using fast CNF satisfiability solvers, and pioneered the use of CounterExample-Guided-Abstraction-Refinement (CEGAR). In addition, Clarke and his students developed the first parallel general resolution theorem prover (Parthenon), and the first theorem prover to be based on a symbolic computation system (Analytica).
  
  Dr. Clarke is one of the founders of the conference on Computer Aided Verification (CAV) and served on its steering committee for many years. He is the former editor-in-chief of Formal Methods in Systems Design. He served on the editorial boards of Distributed Computing, Logic and Computation, and IEEE Transactions in Software Engineering. In 1995 he received a Technical Excellence Award from the Semiconductor Research Corporation. He was a co-recipient of the ACM Kanellakis Award in 1998. 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. 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 co-recipient 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. He received the 2008 CADE Herbrand Award for Distinguished Contributions to Automated Reasoning and a 2010 LICS Test-of-Time Award. In 2011 he was elected to the American Academy of Arts and Sciences. He received an Honorary Doctorate from the Vienna University of Technology in 2012. Dr. Clarke is a Fellow of the ACM and the IEEE, and a member of Sigma Xi and Phi Beta Kappa.
  
  
• Peter Stuckey (NICTA and University of Melbourne, Australia)
  
  Talk title: There Are No CNF problems
  
  Abstract: SAT technology has improved markedly in the last 12 years, to the point where it can solve CNF problems of immense size. Hence it is now a generic tool for tackling many combinatorial satisfaction and optimization problems. But solving CNF problems ignores one important fact: the are NO problems that are originally CNF. The CNF that SAT solvers tackle is the result of modelling a real world problem, mapping the real world constraints into binary decisions, and the complex constraints into possible very large sets of clauses. By throwing away this high level view of the problem SAT solving has been able to concentrate on solving a very tightly defined problem, and doing it very effectively, but it has also lost a lot of knowledge about the problem. Constraint programming is a very flexible approach to modelling and solving combinatorial problems, which makes use of the high level structure of the problem. Modern CP solvers make use of SAT solving technology to solve most effectively, but without throwing away the structure. In this talk I hope to convince you that noone should solve a CNF problem per se. We can reason about the high level structure of a problem to both (a) improve the mapping of the complex constraints to clauses, and more importantly, during runtime choose how we wish to map complex constraints to clauses, and indeed if we should. In this manner we can gain the benefit of both the complex reasoning possible on the high level model, and the SAT style reasoning on the low level model. And if that sounds like SMT, well its closely related, but CP concentrates on individual propagators, with a rich language of communication at the SAT level, between each propagator, while SMT concentrates on putting all the constraints of one form in a theory to reason about them conjunctively. CP concentrates on complex propagators like alldifferent that reflect some substructure (assignment subproblem) of the overall problem, rather than theories for classes of constraints which have some tractable reasoning.
  
  Bio: Professor Peter J. Stuckey is a Professor in the Department of Computing and Information Systems in the University of Melbourne, and project leader in the National ICT Australia Victoria laboratory. Peter Stuckey is a pioneer in constraint programming, the science of modelling and solving complex combinatorial problems. His research interests include: constraint programming; programming languages, in particular declarative programing languages; constraint solving algorithms; bioinformatics; and constraint-based graphics. He enjoys problem solving in any area, having publications in e.g. databases, timetabling, and system security.
  
  Peter Stuckey received a B.Sc and Ph.D both in Computer Science from Monash University in 1985 and 1988 respectively. In 2009 he was recognized as an ACM Distinguished Scientist. In 2010 he was awarded the Google Australia Eureka Prize for Innovation in Computer Science for his work on lazy clause generation. He was awarded the 2010 University of Melbourne Woodward Medal for most outstanding publication in Science and Technology across the university.