skip to main content
10.1145/1173706.1173725acmconferencesArticle/Chapter ViewAbstractPublication PagesgpceConference Proceedingsconference-collections
Article

A generic annotation inference algorithm for the safety certification of automatically generated code

Published: 22 October 2006 Publication History

Abstract

Code generators for realistic application domains are not directly verifiable in practice. In the certifiable code generation approach the generator is extended to generate logical annotations (i.e., pre- and postconditions and loop invariants) along with the programs, allowing fully automated program proofs of different safety properties. However, this requires access to the generator sources, and remains difficult to implement and maintain because the annotations are cross-cutting concerns, both on the object-level (i.e., in the generated code) and on the meta-level (i.e., in the generator).Here we describe a new generic post-generation annotation inference algorithm that circumvents these problems. We exploit the fact that the output of a code generator is highly idiomatic, so that patterns can be used to describe all code constructs that require annotations. The patterns are specific to the idioms of the targeted code generator and to the safety property to be shown, but the algorithm itself remains generic. It is based on a pattern matcher used to identify instances of the idioms and build a property-specific abstracted control flow graph, and a graph traversal that follows the paths from the use nodes backwards to all corresponding definitions, annotating the statements along these paths. This core is instantiated for two generators and successfully applied to automatically certify initialization safety for a range of generated programs.

References

[1]
www.coverity.com.]]
[2]
www.mathworks.com/products/rtw/]]
[3]
XML Path Language (XPath) Version 1.0, 1999. www.w3.org/TR/xpath.]]
[4]
D. Abrahams and A. Gurtovoy. C++ Template Metaprogramming. Addison-Wesley, 2005.]]
[5]
K. Czarnecki and U. W. Eisenecker. Generative Programming: Methods, Tools, and Applications. Addison-Wesley, 2000.]]
[6]
E. Denney and B. Fischer. Correctness of source-level safety policies. In FM'03, LNCS 2805, pp. 894--913. Springer, 2003.]]
[7]
E. Denney and B. Fischer. Certifiable program generation. In GPCE'05, LNCS 3676, pp. 17--28. Springer, 2005.]]
[8]
E. Denney, B. Fischer, and J. Schumann. Adding assurance to automatically generated code. In 8th Intl. Symp. High-Assurance Systems Engineering, pp. 297--299. IEEE Press, 2004.]]
[9]
E. Denney and B. Fischer. A program certification assistant based on fully automated theorem provers. In Intl. Workshop User Interfaces for Theorem Provers, pp. 98--116, April 2005.]]
[10]
E. Denney, B. Fischer, and J. Schumann. An empirical evaluation of automated theorem provers in software certification. Intl. J. of AI Tools, 15(1):81--107, 2006.]]
[11]
N. Dershowitz and Z. Manna. Inference rules for program annotation. ICSE-3, pp. 158--167. IEEE Press, 1978.]]
[12]
M. D. Ernst, J. Cockrell, W. G. Griswold, and D. Notkin. Dynamically discovering likely program invariants to support program evolution. IEEE TSE, 27(2):1--25, 2001.]]
[13]
B. Fischer and J. Schumann. AutoBayes: A system for generating data analysis programs from statistical models. J. Functional Programming, 13(3):483--508, 2003.]]
[14]
C. Flanagan and K. R. M. Leino. Houdini, an annotation assistant for ESC/Java. In FME'01, LNCS 2021, pp. 500--517. Springer, 2001.]]
[15]
C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, and R. Stata. Extended static checking for Java. In PLDI'02, pp. 234--245. ACM Press, 2002.]]
[16]
M.-J. Harrold and G. Rothermel. Syntax-directed construction of program dependence graphs. Technical Report OSU-CISRC-5/96-TR32, The Ohio State University, 1996.]]
[17]
S. Katz and Z. Manna. Logical analysis of programs. CACM, 19(4):188--206, 1976.]]
[18]
O. Lee, H. Yang, and K. Yi. Automatic Verification of Pointer Programs Using Grammar-Based Shape Analysis. In ESOP'05, LNCS 3444, pp. 124--240. Springer, 2005.]]
[19]
J. C. Mitchell. Foundations for Programming Languages. The MIT Press, 1996.]]
[20]
G. C. Necula. Proof-carrying code. In POPL-24, pp. 106--19. ACM Press, 1997.]]
[21]
J. W. Nimmer and M. D. Ernst. Static verification of dynamically detected invariants: Integrating Daikon and ESC/Java. In First Workshop on Runtime Verification, Elec. Notes in Theoretical Computer Science, 55(2). Elsevier, 2001.]]
[22]
C. Rich and L. M. Wills. Recognizing a program's description: A graph-parsing approach. IEEE Software, 7(1):82--89, 1990.]]
[23]
D. R. Smith. KIDS: A semi-automatic program development system. IEEE TSE, 16(9):1024--1043, 1990.]]
[24]
M. Stickel et al. Deductive composition of astronomical software from subroutine libraries. In CADE-12, LNAI 814, pp. 341--355. Springer, 1994.]]
[25]
I. Stürmer and M. Conrad. Test suite design for code generation tools. In ASE-18 pp. 286--290. IEEE, 2003.]]
[26]
B. Wegbreit. The synthesis of loop predicates. CACM, 17(2):102--112, 1974.]]
[27]
M. Whalen, J. Schumann, and B. Fischer. Synthesizing certified code. In FME'02, LNCS 2391, pp. 431--450. Springer, 2002.]]
[28]
J. Whittle and J. Schumann. Automating the implementation of Kalman filter algorithms. ACM Trans. Mathematical Software, 30(4):434--453, 2004.]]

Cited By

View all
  • (2024)An Exercise in Mind Reading: Automatic Contract Inference for Frama-CGuide to Software Verification with Frama-C10.1007/978-3-031-55608-1_13(553-582)Online publication date: 10-Jul-2024
  • (2020)Constraint-Based Contract Inference for Deductive VerificationDeductive Software Verification: Future Perspectives10.1007/978-3-030-64354-6_6(149-176)Online publication date: 4-Dec-2020
  • (2014)Verifying while loops with invariant relationsInternational Journal of Critical Computer-Based Systems10.1504/IJCCBS.2014.0595965:1/2(78-102)Online publication date: 1-Mar-2014
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
GPCE '06: Proceedings of the 5th international conference on Generative programming and component engineering
October 2006
310 pages
ISBN:1595932372
DOI:10.1145/1173706
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 22 October 2006

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. automated code generation
  2. automated theorem proving
  3. hoare calculus
  4. logical annotations
  5. program verification
  6. software certification

Qualifiers

  • Article

Conference

GPCE06
Sponsor:
GPCE06: Generative Programming and Component Engineering 2006
October 22 - 26, 2006
Oregon, Portland, USA

Acceptance Rates

Overall Acceptance Rate 56 of 180 submissions, 31%

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)3
  • Downloads (Last 6 weeks)0
Reflects downloads up to 13 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2024)An Exercise in Mind Reading: Automatic Contract Inference for Frama-CGuide to Software Verification with Frama-C10.1007/978-3-031-55608-1_13(553-582)Online publication date: 10-Jul-2024
  • (2020)Constraint-Based Contract Inference for Deductive VerificationDeductive Software Verification: Future Perspectives10.1007/978-3-030-64354-6_6(149-176)Online publication date: 4-Dec-2020
  • (2014)Verifying while loops with invariant relationsInternational Journal of Critical Computer-Based Systems10.1504/IJCCBS.2014.0595965:1/2(78-102)Online publication date: 1-Mar-2014
  • (2013)Invariant assertions, invariant relations, and invariant functionsScience of Computer Programming10.1016/j.scico.2012.05.00678:9(1212-1239)Online publication date: Sep-2013
  • (2013)Invariant functions and invariant relationsJournal of Symbolic Computation10.1016/j.jsc.2012.04.00148(1-36)Online publication date: 1-Jan-2013
  • (2012)Invariant relations, invariant functions, and loop functionsInnovations in Systems and Software Engineering10.1007/s11334-012-0189-08:3(195-212)Online publication date: 1-Sep-2012
  • (2012)Maximal and Compositional Pattern-Based Loop InvariantsFM 2012: Formal Methods10.1007/978-3-642-32759-9_7(37-51)Online publication date: 2012
  • (2010)Deriving safety cases for hierarchical structure in model-based developmentProceedings of the 29th international conference on Computer safety, reliability, and security10.5555/1886301.1886309(68-81)Online publication date: 14-Sep-2010
  • (2010)Reflexive transitive invariant relationsJournal of Symbolic Computation10.1016/j.jsc.2008.11.00745:11(1114-1143)Online publication date: 1-Nov-2010
  • (2010)Deriving Safety Cases for Hierarchical Structure in Model-Based DevelopmentComputer Safety, Reliability, and Security10.1007/978-3-642-15651-9_6(68-81)Online publication date: 2010
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media