Abstrakt. Vi startade nyligen Formalin-projektet för att skapa en formell version av C99-standarden för C-programmeringsspråket. Vi skriver tre motsvarande formaliseringar för de interaktiva teoremtestarna HOL4, Isabelle/HOL och Coq, som alla följer den befintliga standardtexten C99. Projektet löper från 2011 till 2015 och involverar en heltidsdoktorand, en halvtidsforskare och flera vetenskapliga rådgivare. Projektet skiljer sig från befintligt arbete genom att vårt mål är att formalisera den fullständiga C99-standarden. Detta innebär att vi behandlar C-förprocessorn, C-standardbiblioteket, flyttalsaritmetik och "smutsiga" C-funktioner som signalhantering och flyktiga variabler. Viktigt, detta innebär att vi också behandlar inbäddade C-program utan explicit input/output. De fem första personerna är från Radboud University i Nederländerna. De två första personerna är utvecklarna, medan de andra sex är rådgivare. C-programmeringsspråket [8] är ett av de mest populära i världen. Det är bland de två för närvarande mest populära språken [9, 13], och är ett dominerande språk från den minsta mikrocontroller med bara några hundra byte RAM till den största superdatorn som körs på petaflops hastigheter. C används särskilt för inbäddad programvara, men det är också modersmålet för de flesta moderna operativsystem på grund av dess täta anslutning till Unix. Den nuvarande officiella beskrivningen av syntax och semantik av C-språket - C99-standarden [5], utfärdad av ANSI och ISO tillsammans - är skriven på engelska och inte använder en matematiskt exakt formalism. Detta gör det naturligt
Formalin-projektet REF är en annan formalisering av C-språket.
A Formalization of the C99 Standard in HOL, Isabelle and Coq
{'venue': 'Calculemus/MKM', 'journal': None, 'mag_field_of_study': ['Computer Science']}