Invited Speakers

Sophie Tourret, Inria

The Hows and Whys of Higher-Order SMT

SMT solving for higher order logic has been around for a few years and many challenges remain to tackle. In this talk, I will present an assessment of the current state of research in higher-order SMT and focus on the challenge of quantifier instantiation, following a conflict-based approach inspired from first-order logic.

Mathias Preiner, Stanford University

Challenges in Bit-Vector Reasoning

The theory of fixed-size bit-vectors in Satisfiability Modulo Theories is essential in bit-precise reasoning applications. The dominant state-of-the-art approach for solving bit-vector formulas is a technique called bit-blasting, an eager reduction of bit-vectors to SAT. While surprisingly efficient in practice, bit-blasting may not scale for large bit-vectors or if bit-vector arithmetic is involved. In this talk, I will highlight challenges in reasoning over bit-vectors and discuss the current state of bit-level and word-level approaches.