Keynote and Presentations at CAV 2026

Maria Christakis delivered the keynote lecture “Deriving Test Oracles for Verification Infrastructure” at CAV 2026. Her talk examined the reliability of program analyzers and solvers, which have become essential components of modern software verification. These tools prove safety properties, detect bugs, discharge verification conditions and support automated-reasoning pipelines. Yet they are themselves complex software systems and may contain defects. Because fully verifying every component of a modern verification stack is rarely feasible, the keynote addressed a fundamental question: how can we effectively test the tools used to verify programs?

A central difficulty is the oracle problem: for many complex test inputs, the expected result is not known in advance. Christakis presented several methods for deriving reliable test oracles, including specification-based testing, program generation, differential testing and metamorphic testing. She also discussed interrogation testing, an adaptive approach that uses a system’s previous responses to generate follow-up queries and reveal inconsistencies or contradictions. The talk showed that this oracle-centred perspective extends beyond traditional program analyzers to zero-knowledge systems, compilers for secure multiparty computation and machine-learning models. Across these domains, the aim is to make correctness claims testable by turning the outputs, behaviours and artefacts exposed by complex systems into effective test oracles.

Ivana Bocevska presented “Lagrangian-Based Duality for Quantified SMT Algorithms”, reporting research conducted by an international team from Austria, Japan and Israel. The team also included Takeshi Tsukada (Chiba University), Hiroshi Unno (Tohoku University), Oded Padon (Weizmann Institute of Science) and Sharon Shoham (Tel Aviv University). The study applies ideas from mathematical optimisation to the analysis of algorithms used in program verification and automated reasoning, where complex logical formulas must be solved efficiently and reliably. The researchers showed that three recently proposed algorithms for quantified linear real arithmetic share the same basic structure and differ mainly in how they simplify quantified formulas through a technique known as model-based projection. This common perspective makes it easier to compare the algorithms, understand their strengths and identify their limitations. During the analysis, the team discovered a problem affecting the progress guarantee of one of the methods, proposed a correction and demonstrated experimentally that the revised algorithm performs better. The study also highlights an important open question: whether model-based projection can be implemented efficiently for general formulas and models, rather than only under carefully controlled conditions. The findings provide a clearer foundation for designing more systematic, reliable and efficient solving techniques. The software and experimental artefacts used in the evaluation are publicly available through GitHub and Zenodo.

Georg Weissenbacher contributed to the study “Consistency-Based Software Diagnosis: Accuracy, Scalability, and Limitations,” co-authored with Sarah Sallinger (TU Wien), Lukas Graussam (TU Wien), Florian Zuleger (TU Wien and Technical University of Munich), and Alexey Ignatiev (Monash University, Australia). The research examines consistency-based diagnosis, a formal method for locating software faults by identifying program components whose modification would restore correctness in failing executions. Building on tools such as BugAssist and CFaults, the authors introduce SherLoc, a diagnosis engine for ANSI C programs with multiple failing test cases. SherLoc incorporates an explicit repair model for pointers and arrays, ensuring that the proposed diagnoses correspond to semantically valid C repairs, and adapts efficient algorithms from hardware diagnosis to avoid costly self-composition. On standard benchmarks, the new approach substantially outperforms existing tools. The study also identifies fundamental limitations of formal fault localisation: semantics-preserving program optimisations may invalidate diagnoses, function inlining can produce repairs that cannot be implemented at source level, and bounded encodings may miss faults involving loops or unbounded behaviour. By clarifying the gap between theoretically sound and complete diagnosis and the guarantees that current techniques can realistically provide, the work offers guidance for developing more scalable, robust and principled approaches to automated software diagnosis.