This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Do You Trust Your Compiler?
May 1999 (vol. 32 no. 5)
pp. 65-73

As our society becomes more technologically complex, computer systems are finding an alarming number of uses in safety-critical applications. In many such systems, the software component's reliability is essential to the system's safe operation, so it becomes natural to ask, "How can software be made to behave correctly when executed?" Using program transformations to produce trusted software simplifies verification. Program transformations use proven laws to manipulate programs in a manner analogous to algebraic transformations. The authors have sketched how a formal method based on program transformations can be used to construct a verified compiler. Such a compiler has been proved to correctly compile any correct program into assembly language. While the compiler itself may not execute efficiently-- after all, you need only use the verified compiler the last time you compile a program--the transformational approach should enable the verified compiler to produce efficient assembly code.

Citation:
James M. Boyle, R. Daniel Resler, Victor L. Winter, "Do You Trust Your Compiler?," Computer, vol. 32, no. 5, pp. 65-73, May 1999, doi:10.1109/2.762804
Usage of this product signifies your acceptance of the Terms of Use.