Cubicle-W: Parameterized Model Checking on Weak Memory

Sylvain Conchon, David Declerck and Fatiha Zaidi

A SAT-Based Approach to Learn Explainable Decision Sets

Alexey Ignatiev, Filipe Pereira, Nina Narodytska and Joao Marques-Silva

Probably Half True: Probabilistic Satisfiability over Lukasiewicz Infinitely-valued Logic

Marcelo Finger and Sandro Preto

Symbolic Computation Techniques in SMT Solving: Mathematical Beauty meets Efficient Heuristics

Erika Abraham

A Generic Framework for Implicate Generation Modulo Theories

Mnacho Echenim, Nicolas Peltier and Yanis Sellami

Superposition with Datatypes and Codatatypes

Jasmin Christian Blanchette, Nicolas Peltier and Simon Robillard

MaedMax: A Maximal Ordered Completion Tool

Sarah Winkler and Georg Moser

Constructive Decision via Redundancy-free Proof-Search

Dominique Larchey-Wendling

An abstraction-refinement framework for reasoning with large theories

Julio Cesar Lopez Hernandez and Konstantin Korovin

Uniform Substitution for Differential Game Logic

André Platzer

A Why3 framework for reflection proofs and its application to GMP's algorithms

Guillaume Melquiond and Raphaël Rieu-Helft

A Logical Framework with Commutative and Non-Commutative Subexponentials

Max Kanovich, Stepan Kuznetsov, Vivek Nigam and Andre Scedrov

Complexity of Combinations of Qualitative Constraint Satisfaction Problems

Manuel Bodirsky and Johannes Greiner

An Assumption-Based Approach for Solving The Minimal S5-Satisfiability Problem

Jean Marie Lagniez, Daniel Le Berre, Tiago de Lima and Valentin Montmirail

Deciding the First-Order Theory of an Algebra of Feature Trees with Updates

Nicolas Jeannerod and Ralf Treinen

ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback

Bartosz Piotrowski and Josef Urban

Exploring Approximations for Floating-Point Arithmetic using UppSAT

Peter Backeman, Aleksandar Zeljić, Christoph M. Wintersteiger and Philipp Rümmer

Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories

Katalin Fazekas, Fahiem Bacchus and Armin Biere

Industrial Data Access – What are the Reasoning Problems? And is Reasoning the Problem?

Martin Giese

A New Probabilistic Algorithm for Approximate Model Counting

Cunjing Ge, Feifei Ma, Tian Liu, Jian Zhang and Xutong Ma

Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing

Pei Huang, Feifei Ma, Jian Zhang, Cunjing Ge and Hantao Zhang

FORT 2.0

Franziska Rapp and Aart Middeldorp

Efficient Interpolation for the Theory of Arrays

Jochen Hoenicke and Tanja Schindler

Formalizing Bachmair and Ganzinger's Ordered Resolution Prover

Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel and Uwe Waldmann

Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle

Bohua Zhan and Maximilian Paul Louis Haslbeck

Datatypes with Shared Selectors

Andrew Reynolds, Arjun Viswanathan, Haniel Barbosa, Cesare Tinelli and Clark Barrett

Checking Array Bounds by Abstract Interpretation and Symbolic Expressions

Etienne Payet and Fausto Spoto

Enumerating Justifications using Resolution

Yevgeny Kazakov and Peter Skočovský

Cops and CoCoWeb: Infrastructure for Confluence Tools

Nao Hirokawa, Julian Nagele and Aart Middeldorp

Efficient Model Construction for Horn Logic with VLog: System Description

Jacopo Urbani, Markus Krötzsch, Ceriel Jacobs, Irina Dragoste and David Carral

A Coinductive Approach to Proving Reachability in Logically Constrained Term Rewriting Systems

Stefan Ciobaca and Dorel Lucanu

A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems

Martin Bromberger

Theories as Types

Dennis Müller, Florian Rabe and Michael Kohlhase

Superposition for Lambda-Free Higher-Order Logic

Alexander Bentkamp, Jasmin Christian Blanchette, Simon Cruanes and Uwe Waldmann

Efficient encodings of first-order Horn formulas in equational logic

Nicholas Smallbone and Koen Claessen

A Separation Logic with Data: Small Models and Automation

Jens Katelaan, Dejan Jovanović and Georg Weissenbacher

Extended Resolution Simulates DRAT

Benjamin Kiesl, Adrián Rebola-Pardo and Marijn Heule

Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions

Son Ho, Oskar Abrahamsson, Ramana Kumar, Magnus O. Myreen, Yong Kiam Tan and Michael Norrish

A FOOLish Encoding of the Next State Relations of Imperative Programs

Evgenii Kotelnikov, Laura Kovacs and Andrei Voronkov