WG211/M21Zaytsev

We have analysed hundreds of papers of CAV and TACAS from recent years, and extracted information about 420+ tools used in them. Some of these tools are inaccessible even a year or two after publication, others refer to repositories that are still regularly updated today. Our classification allows outsiders to navigate the overly complex world of program verification and find their way towards actively maintained tools as well as prototypes, and links tools by domain, by common methods and techniques, eventually also by creators. Additionally, a classification we propose, based on the state of the art in knowledge complexity of interactive proof systems, can be used to quickly position any existing tools against the rest of the available verification arsenal, and find blank spots to investigate further.