Advertisement

Certifiable Program Generation

  • Ewen Denney
  • Bernd Fischer
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3676)

Abstract

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.

Keywords

Program Generation Deductive System Safety Property Code Fragment Automate Theorem Prover 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [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
  2. [CL+00]
    Colby, C., Lee, P., Necula, G.C., Blau, F., Plesko, M., Cline, K.: A certifying compiler for Java. In: Proc. ACM Conf. Programming Language Design and Implementation 2000, pp. 95–107. ACM Press, New York (2000); Published as SIGPLAN Notices 35(5)CrossRefGoogle Scholar
  3. [DF03]
    Denney, E., Fischer, B.: Correctness of Source-Level Safety Policies. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 894–913. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  4. [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
  5. [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
  6. [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
  7. [FS03]
    Fischer, B., Schumann, J.: AutoBayes: A System for Generating Data Analysis Programs from Statistical Models. J. Functional Programming 13(3), 483–508 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  8. [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
  9. [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
  10. [MI+97]
    Moser, M., Ibens, O., Letz, R., Steinbach, J., Goller, C., Schumann, J., Mayr, K.: The Model Elimination Provers SETHEO and E-SETHEO. J. Automated Reasoning 18, 237–246 (1997)CrossRefGoogle Scholar
  11. [Mit96]
    Mitchell, J.C.: Foundations for Programming Languages. MIT Press, Cambridge (1996)Google Scholar
  12. [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
  13. [NL98]
    Necula, G.C., Lee, P.: The Design and Implementation of a Certifying Compiler. In: Cooper, K.D. (ed.) Proc. ACM Conf. Programming Language Design and Implementation 1998, vol. (5), pp. 333–344. ACM Press, New York (1998); Published as SIGPLAN Notices 33(5)CrossRefGoogle Scholar
  14. [RTC92]
    RTCA Special Committee 167. Software Considerations in Airborne Systems and Equipment Certification. Technical report, RTCA, Inc. (December 1992)Google Scholar
  15. [Smi90]
    Smith, D.R.: KIDS: A Semi-Automatic Program Development System. IEEE Trans. Software Engineering 16(9), 1024–1043 (1990)CrossRefGoogle Scholar
  16. [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
  17. [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
  18. [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
  19. [WS04]
    Whittle, J., Schumann, J.: Automating the Implementation of Kalman Filter Algorithms. ACM Transactions on Mathematical Software 30(4), 434–453 (2004)zbMATHCrossRefMathSciNetGoogle Scholar
  20. [WSF02]
    Whalen, M., Schumann, J., Fischer, B.: Synthesizing Certified Code. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 431–450. Springer, Heidelberg (2002)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Ewen Denney
    • 1
  • Bernd Fischer
    • 1
  1. 1.NASA Ames Research CenterUSRA/RIACSMoffett FieldUSA

Personalised recommendations