Accepted Papers
Regular Papers
Kneecap: Model-based Generation of Network Traffic
Nik Sultana and Richard Mortier
Computing a Complete Basis for Equalities Implied by a System of LRA Constraints
Martin Bromberger and Christoph Weidenbach
Scrambling and Descrambling SMT-LIB Benchmarks
Tjark Weber
Algebraic Polynomial-based Synthesis for Abstract Boolean Network Analysis
Peter Backeman, Christoph M. Wintersteiger, Boyan Yordanov and Sara-Jane Dunn
LOIS: an application of SMT solvers
Eryk Kopczynski and Szymon Toruńczyk
Extended Abstracts
Reasoning with Sets and Sums of Sets
Markus Bender
Satisfiability Modulo Free Data Structures Combined with Bridging Functions
Raphael Berthon and Christophe Ringeissen
On Intervals and Bounds in Bit-vector Arithmetic
Mikolas Janota and Christoph M. Wintersteiger
On the Benefits of Enhancing Optimization Modulo Theories with Sorting Networks for MaxSMT
Roberto Sebastiani and Patrick Trentin
Presentation-only Papers
Clause Sharing and Partitioning for Cloud-Based SMT Solving
Matteo Marescotti, Antti Hyvärinen and Natasha Sharygina
Deciding Bit-Vector Formulas with mcSAT
Aleksandar Zeljić, Christoph M. Wintersteiger and Philipp Ruemmer
Z3str2+BV: A Solver for a Theory of Strings and Bit-vectors
Murphy Berzish, Sanu Subramanian, Yunhui Zheng, Omer Tripp and Vijay Ganesh
MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures
Curtis Bright, Vijay Ganesh, Albert Heinle, Ilias Kotsireas, Saeed Nejati and Krzysztof Czarnecki
Synthesis of Domain Specific CNF Encoders for Bit-Vector Solvers
Jeevana Priya Inala, Rohit Singh and Armando Solar-Lezama
Proof Certificates for SMT-based Model Checkers
Alain Mebsout and Cesare Tinelli
