Cargando…

Dartagnan: Leveraging Compiler Optimizations and the Price of Precision (Competition Contribution)

We describe the new features of the bounded model checker Dartagnan for SV-COMP ’21. We participate, for the first time, in the ReachSafety category on the verification of sequential programs. In some of these verification tasks, bugs only show up after many loop iterations, which is a challenge for...

Descripción completa

Detalles Bibliográficos
Autores principales: Ponce-de-León, Hernán, Haas, Thomas, Meyer, Roland
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2021
Materias:
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7984541/
http://dx.doi.org/10.1007/978-3-030-72013-1_26