In computing

Computing

Computing is usually defined as the activity of using and improving computer hardware and software. It is the computer-specific part of information technology...

, compiler correctness is the branch of software engineering that deals with trying to show that a compiler

Compiler

A compiler is a computer program that transforms source code written in a programming language into another computer language...

 behaves according to its language specification

Programming language

A programming language is an artificial language designed to communicate instructions to a machine, particularly a computer. Programming languages can be used to create programs that control the behavior of a machine and/or to express algorithms precisely....

. Techniques include developing the compiler using formal methods

Formal methods

In computer science and software engineering, formal methods are a particular kind of mathematically-based techniques for the specification, development and verification of software and hardware systems...

 and using rigorous testing (often called compiler validation) on an existing compiler.

Formal methods

Compiler validation with formal methods involves a long chain of formal, deductive logic. However, since the tool to find the proof (theorem prover) is implemented in software and is complex, there is a high probability it will contain errors. One approach has been to use a tool that verifies the proof (a proof checker) which because it is much simpler than a proof-finder is less likely to contain errors.

A language described as a subset of C

C (programming language)

C is a general-purpose computer programming language developed between 1969 and 1973 by Dennis Ritchie at the Bell Telephone Laboratories for use with the Unix operating system....

 has been formally verified (although no proof was given of its connection to the C Standard), and the proof has been machine checked.

Methods include model checking

Model checking

In computer science, model checking refers to the following problem:Given a model of a system, test automatically whether this model meets a given specification....

 and formal verification

Formal verification

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics .- Usage :Formal verification can be...

.

Testing

Testing represents a significant portion of the effort in shipping a compiler, but receives comparatively little coverage in the standard literature. The 1986 edition of Aho, Sethi, & Ullman has a single-page section on compiler testing, with no named examples. The 2006 edition omits the section on testing, but does emphasize its importance: “Optimizing compilers are so difficult to get right that we dare say that no optimizing compiler is completely error-free! Thus, the most important objective in writing a compiler is that it is correct.”
Fraser & Hanson 1995 has a brief section on regression testing

Regression testing

Regression testing is any type of software testing that seeks to uncover new errors, or regressions, in existing functionality after changes have been made to a system, such as functional enhancements, patches or configuration changes....

; source code is available.
Bailey & Davidson 2003 cover testing of procedure calls
A number of articles confirm that many released compilers have significant code-correctness bugs.
Sheridan 2007 is probably the most recent journal article on general compiler testing.
Commercial compiler compliance validation suites are available from ACE , Perennial, and Plum-Hall,.
For most purposes, the largest body of information available on compiler testing are the Fortran and Cobol validation suites.