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].
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
CASC-JC Theorem Proving Competition. http://www.cs.miams.edu/~tptp/CASC/JC, 2001.
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.
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.
C. Kreitz. “Program Synthesis”. In W. Bibel and P. H. Schmitt, (eds.), Automated Deduction —A Basis for Applications, Vol III, pp. 105–134. 1998.
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.
G. C. Necula. “Proof-Carrying Code”. Proc. 24th POPL, pp. 106–119. 1997.
PolySpace Technologies. http://www.polyspace.com, 2002.
S. Schulz. “System Abstract: E 0.3”. Proc. 16th CADE, LNAI 1421, pp. 297–301. 1999.
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.
C. Weidenbach, B. Gaede, and G. Rock. “Spass and Flotter version 0.42”. Proc. 13th CADE, LNAI 1104, pp. 141–145. 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Whalen, M., Schumann, J., Fischer, B. (2002). AutoBayes/CC — Combining Program Synthesis with Automatic Code Certification — System Description —. In: Voronkov, A. (eds) Automated Deduction—CADE-18. CADE 2002. Lecture Notes in Computer Science(), vol 2392. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45620-1_25
Download citation
DOI: https://doi.org/10.1007/3-540-45620-1_25
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43931-8
Online ISBN: 978-3-540-45620-9
eBook Packages: Springer Book Archive