Konferenzbeitrag
CoVEGI: Cooperative Verification via Externally Generated Invariants
Lade...
Volltext URI
Dokumententyp
Text/Conference Paper
Dateien
Zusatzinformation
Datum
2022
Autor:innen
Zeitschriftentitel
ISSN der Zeitschrift
Bandtitel
Quelle
Verlag
Gesellschaft für Informatik e.V.
Zusammenfassung
Software verification has recently made enormous progress. To keep their tools up to date with novel methods and enhanced techniques, tool developers integrate these within their own framework almost exclusively by re-implementation. While this allows for a conceptual re-use of methods, it nevertheless requires novel implementations. Our configurable framework named CoVEGI employs cooperative verification in order to avoid re-implementation and enable usage of novel tools as black-box components in verification. Specifically, cooperation is employed for invariant generation, which is key to the success of a verification run. CoVEGI allows a main verification tool to delegate the task of invariant generation to one or several specialized helper invariant generators, utilizing their results within its verification run. The experimental evaluation shows that the use of CoVEGI can increase the number of correctly verified tasks up to 17%, without increasing the used resources.