In the past decades we have witnessed major advances in the power of automated reasoning engines like Satisfiability Modulo Theories (SMT) and Horn clause solvers. As a consequence, there has been a renaissance of software verification based on this technology. Currently, there are a number of mature verifiers available coming both from academia and industry. However, despite these advances, the bar for newcomer researchers to contribute to this field is still very high. One of the main obstacles is the very large cost of development of a new software verifier from scratch. Hence, several groups have been independently working on implementing open software verification infrastructures, which would allow for easier prototyping of research ideas in this space, e.g., new algorithms for verifying relational or timing properties, thereby democratizing software verification.
This workshop aims to bring together the developers of open software verification infrastructures and their potential clients, meaning researchers and practitioners interested in developing prototypes of software verification algorithms. We will structure the workshop to facilitate the exchange of ideas and discussions between the developers and clients. Hence, the workshop will include invited talks on core verification infrastructures as well as presentations of projects that already leverage these infrastructures. We also hope to attract potential new clients as well, who would present the requirements of their projects through a series of lightning talks. Through open discussions we will solicit feedback from the community on the requirements and functionality that open research infrastructures should include to make them more widely usable.
As further discussion topics, we will solicit talks and feedback on benchmarking issues, reproducibility, input languages, and potential license issues, all of which are important to have a viable software verification research ecosystem that can be leveraged by both industry and academia.
The Technion, Haifa, Israel
Please register for the workshop through the FLoC registration page.
This workshop will be held on August 11, 2022, and colocated with the 34th International Conference on Computer-Aided Verification (CAV). The workshop is chaired by developers of SMACK and SeaHorn:
- Michael Emmi, Amazon Web Services
- Arie Gurfinkel, University of Waterloo
- Temesghen Kahsai, Amazon Devices
- Jorge Navas, Certora
- Zvonimir Rakamaric, Amazon Web Services