# Extract, model, refine: improved modelling of program verification tools through data enrichment

## TL;DR

This paper introduces a new model and dataset for program verification tools, helping software engineers choose and compare tools more effectively.

## Contribution

The paper presents a novel megamodel and dataset of program verification tools with automated data enrichment.

## Key findings

- A megamodel was developed to categorize program verification tools based on their characteristics.
- A dataset of over 400 tools was created, including practical details and up-to-date information via APIs.
- Trends in verification tool categories were identified to guide software engineers in selecting appropriate tools.

## Abstract

In software engineering, models are used for many different things. In this paper, we focus on program verification, where we use models to reason about the correctness of systems. There are many different types of program verification techniques which provide different correctness guarantees. We investigate the domain of program verification tools and present a concise megamodel to distinguish these tools. We also present a data set of 400+ program verification tools. This data set includes the category of verification tool according to our megamodel, practical information such as input/output format, repository links and more. The practical information, such as last commit date, is kept up to date through the use of APIs. Moreover, part of the data extraction has been automated to make it easier to expand the data set. The categorisation enables software engineers to find suitable tools, investigate alternatives and compare tools. We also identify trends for each level in our megamodel. Our data set, publicly available at https://doi.org/10.4121/20347950, can be used by software engineers to enter the world of program verification and find a verification tool based on their requirements. This paper is an extended version of https://doi.org/10.1145/3550355.3552426.