Certifiable Program Generation
- 632 Downloads
Code generators based on template expansion techniques are easier to build than purely deductive systems but do not guarantee the same level of assurance: instead of providing “correctness-by-construction”, the correctness of the generated code depends on the correctness of the generator itself. We present an alternative assurance approach, in which the generator is extended to enable Hoare-style safety proofs for each individual generated program. The proofs ensure that the generated code does not “go wrong”, i.e., does not violate certain conditions during its execution.
The crucial step in this approach is to extend the generator in such way that it produces all required annotations (i.e., pre-/postconditions and loop invariants) without compromising the assurance provided by the subsequent verification phase. This is achieved by embedding annotation templates into the code templates, which are then instantiated in parallel by the generator. This is feasible because the structure of the generated code and the possible safety properties are known when the generator is developed. It does not compromise the provided assurance because the annotations only serve as auxiliary lemmas and errors in the annotation templates ultimately lead to unprovable safety obligations.
We have implemented this approach and integrated it into the AutoBayes and AutoFilter program generators. We have then used it to fully automatically prove that code generated by the two systems satisfies both language-specific properties such as array-bounds safety or proper variable initialization-before-use and domain-specific properties such as vector normalization, matrix symmetry, or correct sensor input usage.
KeywordsProgram Generation Deductive System Safety Property Code Fragment Automate Theorem Prover
Unable to display preview. Download preview PDF.
- [BG+98]Blaine, L., Gilham, L.-M., Liu, J., Smith, D.R., Westfold, S.: Planware – Domain-Specific Synthesis of High-Performance Schedulers. In: Redmiles, D.F., Nuseibeh, B. (eds.) Proc. 13th Intl. Conf. Automated Software Engineering, pp. 270–280. IEEE Comp. Soc. Press, Los Alamitos (1998)Google Scholar
- [DFS05]Denney, E., Fischer, B., Schumann, J.: An Empirical Evaluation of Automated Theorem Provers in Software Certification. International Journal of AI Tools (2005) (to appear)Google Scholar
- [FH+03]Fischer, B., Hajian, A., Knuth, K., Schumann, J.: Automatic Derivation of Statistical Data Analysis Algorithms: Planetary Nebulae and Beyond. In: Erickson, G., Zhai, Y. (eds.) Proc. 23rd Intl. Workshop on Bayesian Inference and Maximum Entropy Methods in Science and Engineering, pp. 276–291. American Institute of Physics, New York (2003)Google Scholar
- [FL+02]Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Hendren, J. (ed.) Proc. ACM Conf. Programming Language Design and Implementation 2002, pp. 234–245. ACM Press, New York (2002); Published as SIGPLAN Notices 37(5)CrossRefGoogle Scholar
- [Kre98]Kreitz, C.: Program Synthesis. In: Bibel, W., Schmitt, P.H. (eds.) Automated Deduction — A Basis for Applications, pp. 105–134. Kluwer, Dordrecht (1998)Google Scholar
- [LPR01]Lowry, M., Pressburger, T., Rosu, G.: Certifying Domain-Specific Policies. In: Feather, M.S., Goedicke, M. (eds.) Proc. 16th Intl. Conf. Automated Software Engineering, pp. 118–125. IEEE Comp. Soc. Press, Los Alamitos (2001)Google Scholar
- [Mit96]Mitchell, J.C.: Foundations for Programming Languages. MIT Press, Cambridge (1996)Google Scholar
- [Nec97]Necula, G.C.: Proof-Carrying Code. In: Proc. 24th ACM Symp. Principles of Programming Languages, pp. 106–119. ACM Press, New York (1997)Google Scholar
- [RTC92]RTCA Special Committee 167. Software Considerations in Airborne Systems and Equipment Certification. Technical report, RTCA, Inc. (December 1992)Google Scholar
- [SW+94]Stickel, M., Waldinger, R., Lowry, M., Pressburger, T., Underwood, I.: Deductive Composition of Astronomical Software from Subroutine Libraries. In: Bundy, A. (ed.) CADE 1994. LNCS (LNAI), vol. 814, pp. 341–355. Springer, Heidelberg (1994)Google Scholar
- [WB96]Winter, V.L., Boyle, J.M.: Proving Refinement Transformations for Deriving High-Assurance Software. In: Proc. High-Assurance Systems Engineering Workshop, pp. 68–77. IEEE Comp. Soc. Press, Los Alamitos (1996)Google Scholar
- [WH99]Whalen, M., Heimdahl, M.: On the Requirements of High-Integrity Code Generation. In: Proc. 4th Intl. Symp. High-Assurance Systems Engineering, pp. 216–226. IEEE Comp. Soc. Press, Los Alamitos (1999)Google Scholar