Keynotes

Abstract: Many automated reasoning tasks regularly need to solve NP-hard problems. In that situation it is most natural to employ efficient off-the-shelf SAT solvers after proper encoding and potentially factoring out algorithmically NP-hard subproblems. This approach is used in many reasoners, including model checkers, theorem provers and of course SMT solvers as well as users of those tools. It does benefit from the ever increasing scalability of SAT solvers in particular. In this talk we start from this scalability observation, show some recent developments of SAT solving that help to improve various automated reasoning tasks and then report on robustness of SAT and automated reasoning in general. We finally argue how these observations transfer to beliefs on where on the application side complete and incomplete methods can interact most effectively.

Bio: Since 2021 Professor Armin Biere is leading the Chair of Computer Architecture at the University Freiburg in Germany after 17 years at the Johannes Kepler University in Linz, Austria. His primary research interests are applied formal methods, more specifically formal verification of hardware and software, using model checking and related techniques with the focus on developing efficient SAT and SMT solvers, which reached many top rank international competitions, actually were awarded 113 medals including 63 gold medals. He is a recipient of an IBM faculty award in 2012, received the TACAS most influential paper in the first 20 years of TACAS award in 2014, the HVC’15 award on the most influential work in the last five years in formal verification, simulation, and testing, the ETAPS 2017 Test of Time Award, the CAV Award in 2018, the IJCAI-JAIR 2019 Award, the 1990s Most Influential Paper Award at DAC’23, the SAT’23 Test-of-Time Award, the Herbrand Award at IJCAR’24, and the SAT’25 Test-of-Time Award. Armin Biere was co-chair of SAT’06, FMCAD’09, HVC’12, CAV’14, TACAS’20 and IJCAR’26. He served on the editorial boards of JAR (2011-2021), FMSD (2012-2021), and JAIR (2019-2023), as Associate Editor, as well as on the board of JSAT (since 2004). He is an editor of the Handbook of Satisfiability of the 1st edition 2009 and 2nd in 2021. He initiated and organizes the Hardware Model Checking Competition (HWMCC) from 2007-2025. From 2011-2017 he served as (first) chair and from 2017 to 2020 as vice-chair, now as counselor to the board of the SAT Association. Since 2012 he is a member of the steering committee of FMCAD. In 2006 Armin Biere co-founded NextOp Software Inc. which was acquired by Atrenta Inc. in 2012.

Abstract: Program analysers and solvers are trusted to establish software correctness, yet they are themselves complex software systems. Since fully verifying modern verification infrastructure is rarely realistic, how can we test the tools that verify our programs?

The central challenge is the oracle problem: for many inputs, we do not know what the tool should report. This talk presents a toolbox of complementary techniques for engineering test oracles, including specification-based testing, program generation, differential testing, metamorphic testing, and interrogation testing. I will show how specifications, generated inputs, comparisons, relations between inputs, and information exposed by the tool can be turned into effective checks. Examples from reachability analysis, CHC solving, and taint analysis illustrate how different claims call for different oracle designs.

The lessons extend beyond verification infrastructure to any software system that makes claims others are expected to trust.

Bio: Maria Christakis is a Full Professor at TU Wien, where she leads the Software Engineering Research Unit. She develops techniques and tools for specifying, verifying, analysing, testing, and debugging software, aiming to make programs more robust while improving the developer experience.
Before joining TU Wien in 2022, she conducted research at the Max Planck Institute for Software Systems, the University of Kent, Microsoft Research, and ETH Zurich. She has received an ERC Starting Grant, WWTF and FWF grants, a Google Research Scholar Award, an Amazon Research Award, and the ACM-W Rising Star Award. She was also elected to the Young Academy of the Austrian Academy of Sciences.