The Static Analyzer Frama-C in SV-COMP (Competition Contribution)

Beyer, Dirk und Spiessl, Martin (2022): The Static Analyzer Frama-C in SV-COMP (Competition Contribution). 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2–7, 2022. Fisman, Dana und Rosu, Grigore (Hrsg.): In: Tools and Algorithms for the Construction and Analysis of Systems. 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Proceedings, Part II, Lecture Notes in Computer Science Bd. 13244 Cham: Springer. S. 429-434

Abstract

Frama-C is a well-known platform for source-code analysis of programs written in C. It can be extended via its plug-in architecture by various analysis backends and features an extensive annotation language called ACSL. So far it was hard to compare Frama-C to other software verifiers. Our competition participation contributes an adapter named Frama-C-SV, which makes it possible to evaluate Frama-C against other software verifiers. The adapter transforms standard verification tasks (from the well-known SV-Benchmarks collection) in a way that can be understood by Frama-C and produces a verification witness as output. While Frama-C provides many different analyses, we focus on the Evolved Value Analysis (EVA), which uses a combination of different domains to over-approximate the behavior of the analyzed program.

• Dokumententyp: Konferenzbeitrag (Paper)
• Fakultät: Mathematik, Informatik und Statistik > Informatik
• Themengebiete: 000 Informatik, Informationswissenschaft, allgemeine Werke > 004 Informatik
• ISSN: 0302-9743
• Ort: Cham
• Sprache: Englisch