Advertisement

AutoBayes/CC — Combining Program Synthesis with Automatic Code Certification — System Description —

  • Michael Whalen
  • Johann Schumann
  • Bernd Fischer
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2392)

Abstract

Code certification is a lightweight approach to formally demonstrate software quality. It concentrates on aspects of software quality that can be defined and formalized via properties, e.g., operator safety or memory safety. Its basic idea is to require code producers to provide formal proofs that their code satisfies these quality properties. The proofs serve as certificates which can be checked independently, by the code consumer or by certification authorities, e.g., the FAA. It is the idea underlying such approaches as proof-carrying code [6].

Keywords

Predicate Symbol Domain Theory Proof Obligation Code Fragment Safety Policy 
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. [1]
    CASC-JC Theorem Proving Competition. http://www.cs.miams.edu/~tptp/CASC/JC, 2001.
  2. [2]
    B. Fischer and J. Schumann. AutoBayes: A System for Generating Data Analysis Programs from Statistical Models. JFP, to appear 2002. Preprint available at http://ase.arc.nasa.gov/people/fischer/papers.html.
  3. [3]
    T. Kaiser, B. Fischer, and W. Struckmann. “MOPS: Verifying Modula-2 programs specified in VDM-SL”. Proc. 4th Workshop Tools for System Design and Verification, pp. 163–167, 2000.Google Scholar
  4. [4]
    C. Kreitz. “Program Synthesis”. In W. Bibel and P. H. Schmitt, (eds.), Automated Deduction —A Basis for Applications, Vol III, pp. 105–134. 1998.Google Scholar
  5. [5]
    M. Moser, O. Ibens, R. Letz, J. Steinbach, C. Goller, J. Schumann, and K. Mayr. “The Model Elimination Provers SETHEO and E-SETHEO”. JAR, 18:237–246, 1997.CrossRefGoogle Scholar
  6. [6]
    G. C. Necula. “Proof-Carrying Code”. Proc. 24th POPL, pp. 106–119. 1997.Google Scholar
  7. [7]
    PolySpace Technologies. http://www.polyspace.com, 2002.
  8. [8]
    S. Schulz. “System Abstract: E 0.3”. Proc. 16th CADE, LNAI 1421, pp. 297–301. 1999.Google Scholar
  9. [9]
    G. Stenz and A. Wolf. “E-SETHEO: Design Configuration and Use of a Parallel Theorem Prover”. Proc. 12th Australian Joint Conf. Artificial Intelligence, LNAI 1747, pp. 231–243. 1999.Google Scholar
  10. [10]
    C. Weidenbach, B. Gaede, and G. Rock. “Spass and Flotter version 0.42”. Proc. 13th CADE, LNAI 1104, pp. 141–145. 1996.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Michael Whalen
    • 1
  • Johann Schumann
    • 2
  • Bernd Fischer
    • 2
  1. 1.Department of Computer Science and EngineeringUniv. of MinnesotaMinneapolis
  2. 2.RIACS / NASA AmesMoffett Field

Personalised recommendations