I detta dokument introduceras en metod för att utföra formell verifiering av flyttal C-program. Det utökar ett befintligt verktyg för verifiering av C-program, Caduceus, med nya annoteringar specifika för flyttal aritmetik. Caduceus första-order logik modell för C-program utvidgas därefter. Därefter verifiera villkor som uttrycker korrektheten av programmen erhålls på det vanliga sättet och kan skrivas ut interaktivt med Coq bevis assistent, med hjälp av en befintlig Coq formalisering av flyttal aritmetik. Denna metod är redan implementerad och har framgångsrikt tillämpats på flera korta flyttals program, som presenteras i detta dokument.
I REF utökas Caduceus-verktyget med anledning av flyttalsaritmetik.
Formal Verification of Floating-Point Programs
{'venue': "18th IEEE Symposium on Computer Arithmetic (ARITH '07)", 'journal': "18th IEEE Symposium on Computer Arithmetic (ARITH '07)", 'mag_field_of_study': ['Computer Science']}