Goblint Validator: Correctness Witness Validation by Abstract Interpretation

Simmo Saan, Julian Erhard, Michael Schwarz, Stanimir Bozhilov, Karoliine Holter, Sarah Tilscher, Vesal Vojdani, Helmut Seidl

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

2 Scopus citations

Abstract

Goblint is an abstract interpretation framework for C programs with a specialty in concurrency. Using a novel approach, we turn it into a validator of YAML correctness witnesses for all SV-COMP categories. We describe its results at SV-COMP 2024 which includes the first large-scale evaluation of our validator.

Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Proceedings
EditorsBernd Finkbeiner, Laura Kovács
PublisherSpringer Science and Business Media Deutschland GmbH
Pages335-340
Number of pages6
ISBN (Print)9783031572555
DOIs
StatePublished - 2024
Event30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2024, which was held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024 - Luxembourg City, Luxembourg
Duration: 6 Apr 202411 Apr 2024

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume14572 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2024, which was held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024
Country/TerritoryLuxembourg
CityLuxembourg City
Period6/04/2411/04/24

Fingerprint

Dive into the research topics of 'Goblint Validator: Correctness Witness Validation by Abstract Interpretation'. Together they form a unique fingerprint.

Cite this