Abstracts Talks
| Armin Biere | Efficient SAT Solving |
| This overview talk covers algorithmic aspects of conflict-driven clause learning and important extensions developed in recent years, including decision heuristics, restart schemes, various pre- and inprocessing techniques as well as proof generation and checking. The speaker contributed to the core technology of modern SAT solving, has developed 12 SAT solvers since 1999, which won 40 medals including 18 gold medals in international SAT competitions. |
| Cezary Kaliszyk | Learning Theorem Proving from Scratch |
| We introduce a theorem proving algorithm that integrates machine learning. Instead of a complete brute-force search, the algorithm runs many Monte-Carlo simulations guided by reinforcement learning from previous proof attempts. Various predictors for estimating the usefulness of proof steps and the likelihood of closing the open tableaux branches will be compared. Complete proof search with backtracking will be replaced by Monte-Carlo tree search with upper confidence bounds. The trained system solves within the same number of inferences over 40% more problems than the human-optimized baseline prover. |
| Moshe Vardi | The Siren Song of Temporal Synthesis |
| One of the most significant developments in the area of design verification over the last three decade is the development of algorithmic methods for verifying temporal specification of finite-state designs. A frequent criticism against this approach, however, is that verification is done after significant resources have already been invested in the development of the design. Since designs invariably contains errors, verification simply becomes part of the debugging process. The critics argue that the desired goal is to use temporal specification in the design development process in order to guarantee the development of correct designs. This is called temporal synthesis. In this talk I will review 60 years of research on the temporal synthesis problem, describe the automata-theoretic approach developed to solve this problem, and describe both succuesses and failures of this research program. |
| Christoph Weidenbach | Robust First-Order Reasoning |
| The talk starts by presenting the state of the art in reasoning in first-order logic, fragments thereof and the combination of reasoning in first-order logic with theories such as arithmetic. It then discusses the gap between the state of the art and robust first-order reasoning. The speaker contributed to the core technology of modern first-order reasoning, including the identification of decidable fragments, the development of new calculi, the combination with theories, and the development of systems. Between 1996 and 1999 with his team he competed in the CASC first-order theorem proving competition and won 5 gold medals with SPASS. This year, after almost 20 years without joining any academic system competion, they joined SMT-COMP in the two quantifier free purely linear arithmetic categories, won one and scored second in the other with SPASS-SATT. |