Slides

• Model-Based API Testing for SMT Solvers
  SMT 2017, Heidelberg, Germany.
• Boolector at the SMT competition 2017
  SMT-COMP’17, Heidelberg, Germany
• Counterexample-Guided Model Synthesis
  TACAS’17, Uppsala, Sweden
• Precise and Complete Propagation Based Local Search for Satisfiability Modulo Theories
  CAV 2016, Toronto, Ontario, Canada.
• Better Lemmas with Lambda Extraction
  FMCAD’15, Austin, Texas, USA
• Improving Local Search for Bit-Vector Logics with Path Propagation
  DIFTS 2015, Austin, TX, USA.
• Turbo-Charging Lemmas on Demand with Don’t Care Reasoning
  FMCAD 2014, Lausanne, Switzerland.
• Boolector at the SMT competition 2014
  SMT-COMP’14, Vienna, Austria
• Lemmas on Demand for Lambdas
  DIFTS’13, Portland, Oregon, USA
• Boolector 1.2
  SMT-COMP’09, Montreal, Canada
• Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays
  TACAS’09, York, UK
• Effective Bit-Width and Under-Approximation
  Eurocast’09, Las Palmas de Gran Canaria, Spain
• BTOR: Bit-Precise Modelling of Word-Level Problems for Model Checking
  BPR’08, Princeton, New Jersey, USA
• Lemmas on Demand for the Extensional Theory of Arrays SMT’08, Princeton, New Jersey, USA
• Boolector 0.4
  SMT-COMP’08, Princeton, New Jersey, USA
• Offline SMT for Arrays
  AVM’08, Semmering, Austria