SAtRes    News    Visiting Armin Biere and Robert Jones

Visiting Armin Biere and Robert Jones

June 22, 2026

Last week, SAtRes researchers Ruben Götz and Niccolò Rigi-Luperti visited both Prof. Armin Biere (University of Freiburg) and Robert Jones (AWS Senior Principal Scientist) in Freiburg.

Robert Jones gave an insightful talk on applications of Automated Reasoning at Amazon, which are now used in many of Amazon’s services. A recent example is the use of SMT Solvers for Access Management of AWS S3 Buckets, routinely solving 1 billion SMT queries a day.

We subsequently exchanged and discussed insights and ideas, in particular concerning parallel clause-sharing solving. Robert Jones recently took part in developing a new clause-sharing SMT solver (SMT-D), and it was interesting to discuss which similar observations and questions surfaced there compared to our our massively parallel platform Mallob. Such research is also further supported by our recently received Amazon Research Award for SAT solving in the cloud. With Armin Biere, we were able to discuss his recent insights on the transition from sequential to parallel SAT solving, areas in which he and his group develop state-of-the art and award-winning solvers.