From mboxrd@z Thu Jan 1 00:00:00 1970 MIME-Version: 1.0 In-Reply-To: References: Date: Tue, 22 Sep 2009 17:44:45 -0500 Message-ID: From: Jason Catena To: Fans of the OS Plan 9 from Bell Labs <9fans@9fans.net> Content-Type: text/plain; charset=ISO-8859-1 Subject: Re: [9fans] linux stats in last year from linuxcon Topicbox-Message-UUID: 75f69214-ead5-11e9-9d60-3106f5b1d025 > There were no proofs about the behavior of the C compiler or the underlying cpu. In related news, there is a verified Clight compiler out there for PowerPC machines. Leroy, X. 2009. Formal verification of a realistic compiler. Commun. ACM 52, 7 (Jul. 2009), 107-115. DOI= http://doi.acm.org/10.1145/1538788.1538814 This paper reports on the development and formal verification (proof of semantic preservation) of CompCert, a compiler from Clight (a large subset of the C programming language) to PowerPC assembly code, using the Coq proof assistant both for programming the compiler and for proving its correctness. Such a verified compiler is useful in the context of critical software and its formal verification: the verification of the compiler guarantees that the safety properties proved on the source code hold for the executable compiled code as well. > Tim Newsham Jason Catena