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