Testing Program Analyzers and Verifiers (Dagstuhl Seminar 25242)

This report documents the program and the outcomes of Dagstuhl Seminar 25242 "Testing Program Analyzers and Verifiers". Program analyzers and verifiers are routinely employed during software development to prevent and detect faults. In this seminar, we examine the impact of faults within these tools, distinguishing between those that are critical and those that are less severe. We also explore and discuss state-of-the-art techniques for uncovering faults in program analyzers and verifiers, their connections to related domains such as compiler testing, and potential future directions for improving their reliability.