Bruno Dutertre, SRI International

Bruno Dutertre is a Staff Scientist at SRI International, Menlo Park. CA. His research interests include formal methods and their application to the verification of high-integrity systems. At SRI, he maintains and develops formal methods tools, such as, model checkers and SMT solvers. He is the main developer and maintainer of the Yices 2 SMT Solver.

The Nuts and Bolts of Yices

At a high-level, the architecture of many SMT solvers is well known. It is the combination of a SAT solver and one or more decision procedures called theory solvers. But how to effectively implement such a combination is rarely discussed in the literature. This talk will focus on implementation details. We will discuss data structures and algorithms employed by the Yices SMT Solver, and examine issues such as preprocessing and formula simplification, which have a significant impact on a solver's performance.

Carsten Fuhs, Birkbeck, University of London

Carsten Fuhs is a Lecturer at Birkbeck, University of London, UK. His main areas of research include techniques and tools to automatically (dis-)prove termination of term rewriting systems and programs as well as SAT and SMT encodings. Carsten is one of the main developers of the termination analysis tool AProVE.

SMT Techniques and Solvers in Automated Termination Analysis

Termination is the property of a program that regardless of the input, execution of the program will always come to a halt eventually. Although this property is undecidable, since the early 2000s fully automated techniques and tools for termination analysis have flourished in several communities: term rewriting, imperative programs, functional programs, logic programs, ...

A common theme behind most of these tools is the use of constraint-based techniques to advance the proof of (non-)termination. Recently, in particular SAT and SMT solvers are used as back-ends to automate these techniques. In my talk, I will give an overview of automated termination analysis from an SMT solving perspective.

Justin Pearson, Uppsala University

Justin Pearson is a senior lecturer(Docent) at the department of IT at Uppsala University. His main focus of research is on constraint programming, its theory, solver development, and applications. His work on solver development has included work on propagator design. Propagators are an essential component of a modern constraint solver. He has worked in applications of constraint programming in diverse areas from air-traffic control with Eurocontrol, to software testing with Ericsson.

Constraint Programming - an Introduction, with some Applications to String Processing

In this talk I will give a short introduction to constraint programming with emphasis on global constraints and propagation. Global constraints are a fundamental component of a modern constraint solver that not only allow common combinatorial substructures to be modelled, but they also significantly prune the space. Further will talk about some community wide efforts to standardise solver interfaces (MiniZinc), and some recent work done in Uppsala on constraint programming with bounded strings.