Abstrakt. Vi presenterar ett verktyg för formell verifiering av ANSI-C-program med Bounded Model Checking (BMC). Tyngdpunkten ligger på användbarhet: Verktyget stöder nästan alla ANSI-C språkfunktioner, inklusive pekarkonstruktioner, dynamisk minnesallokering, rekursion, och float och dubbla datatyper. Ur användarens perspektiv är verifieringen mycket automatiserad: den enda inmatning som krävs är BMC-bandet. Verktyget är integrerat i ett grafiskt användargränssnitt. Detta är viktigt för att presentera långa motexempel spår: verktyget tillåter kliva igenom spåret på samma sätt en avlusare tillåter kliva igenom ett program.
CMBC6 är en begränsad modellkontroll för ANSI-C-program, som beskrivs i REF.
A tool for checking ANSI-C programs
{'venue': 'In Tools and Algorithms for the Construction and Analysis of Systems', 'journal': None, 'mag_field_of_study': ['Computer Science']}