TY - GEN
T1 - Panel on compiler certification
T2 - ACM SIGAda's Annual International Conference on High Integrity Language Technology, HILT 2012
AU - Beringer, Lennart
AU - Brukardt, Randall
AU - Plum, Thomas
AU - Taft, S. Tucker
PY - 2012
Y1 - 2012
N2 - Whether programming in a high-level modeling language providing automatic code generation, in a formally-verifiable language, in a language with advanced static analysis tools, or directly in a normal third-generation programming language, we ultimately depend on a compiler to generate the actual machine code that is executed by the target machine. This panel will discuss the issue of how we build trust in our compilers, using a commercial test suite, a standardized test suite, or a formal verification process.
AB - Whether programming in a high-level modeling language providing automatic code generation, in a formally-verifiable language, in a language with advanced static analysis tools, or directly in a normal third-generation programming language, we ultimately depend on a compiler to generate the actual machine code that is executed by the target machine. This panel will discuss the issue of how we build trust in our compilers, using a commercial test suite, a standardized test suite, or a formal verification process.
KW - Ada conformity assessment
KW - compcert
KW - compiler validation suite
KW - formal verification of compilers
UR - http://www.scopus.com/inward/record.url?scp=84871600254&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84871600254&partnerID=8YFLogxK
U2 - 10.1145/2402676.2402708
DO - 10.1145/2402676.2402708
M3 - Conference contribution
AN - SCOPUS:84871600254
SN - 9781450315050
T3 - Proceedings of the ACM SIGAda Annual International Conference; SIGAda
SP - 103
BT - HILT 2012 - Proceedings of the ACM Conference on High Integrity Language Technology
Y2 - 2 December 2012 through 6 December 2012
ER -