Konferenzbeitrag
Visualization Support for Contracts in VeriFast
Vorschaubild nicht verfügbar
Volltext URI
Dokumententyp
Text/Conference Paper
Zusatzinformation
Datum
2023
Zeitschriftentitel
ISSN der Zeitschrift
Bandtitel
Verlag
Gesellschaft für Informatik e.V.
Zusammenfassung
A widespread quality assurance technique for ensuring correctness of software is testing, but relevant test cases might be easily overlooked. Formal methods - an alternative to testing - are applied in software industry only rarely, due to the lack of both widely used verification tools and engineers able to apply such tools effectively. In order to address these problems, our university offers appropriate courses, in which the open-source tool VeriFast is applied to formally verify given contracts for functions implemented in C. While VeriFast is very fast in verifying even larger programs, students often have difficulties when authoring function contracts and other proof arguments formally. To address this problem, we developed a web-based system for visualizing each contract as a graph. In this paper, we describe the architecture and the main features of our system and show on a running example, how our system can support the user of VeriFast.