| 1 | -- | 2 | Sava Krstic, Albert Oliveras. Preface |
| 3 | -- | 17 | Mirron Rozanov, Ofer Strichman. Generating Minimum Transitivity Constraints in P-time for Deciding Equality Logic |
| 19 | -- | 35 | Michal Moskal, Jakub Lopuszanski, Joseph R. Kiniry. E-matching for Fun and Profit |
| 37 | -- | 49 | Leonardo Mendonça de Moura, Nikolaj Bjørner. Model-based Theory Combination |
| 51 | -- | 69 | Sylvain Conchon, Evelyne Contejean, Johannes Kanig, Stéphane Lescuyer. CC(X): Semantic Combination of Congruence Closure with Solvable Theories |
| 71 | -- | 84 | Jeremy Bongio, Cyrus Katrak, Hai Lin, Christopher Lynch, Ralph Eric McGregor. Encoding First Order Proofs in SMT |