Abstrakt. Statiska analysatorer baserade på abstrakt tolkning är komplexa delar av programvara som implementerar känsliga algoritmer. Även om statisk analys teknik är väl förstådd, deras genomförande på verkliga språk är fortfarande fel-benäget. Detta dokument presenterar en formell verifiering med hjälp av Coq proof assistenten: en formalisering av en värdeanalys (baserad på abstrakt tolkning) och en sundhet bevis på värdeanalysen. Formaliseringen bygger på generiska gränssnitt. Den mekaniserade bevis underlättas av en översättning validering av en Bourdoncle fixpoint iterator. Arbetet har integrerats i CompCert verifierad C-kompilator. Vår verifierade analys fungerar direkt över ett mellanliggande språk av kompilatorn med samma uttrycksfullhet som C. Den automatiska extraktionen av vår värdeanalys i OCaml ger ett program med konkurrenskraftiga resultat, som erhållits från experiment på ett antal riktmärken och jämförelser med Frama-C-verktyget.
I ett försök nyligen, Blazy et al. REF undersökte formaliseringen av en värdeanalys för C som integrerats i CompCert-ramen.
Formal Verification of a C Value Analysis Based on Abstract Interpretation
{'venue': 'SAS - 20th Static Analysis Symposium Lecture Notes in Computer Science (2013) 324-344', 'journal': None, 'mag_field_of_study': ['Computer Science']}