Synthesizing certified code

DOI10.1007/3-540-45614-7_25MaRDI QIDQ4808844zbMATH OpenFDO

Authors Johann Schumann, Bernd Fischer, Michael W. Whalen

Publication date 12 August 2004

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2391/23910431.htm, https://eprints.soton.ac.uk/262941/1/whalen-fme.pdf

zbMATH Keywords

automated theorem provingautomatic program synthesiscode certificationprogram verificationproof-carrying code

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• AutoBayes/CC -- combining program synthesis with automatic code certification -- system description
• A generic software safety document generator
• From program verification to program synthesis
• Certifying compilation and run-time code generation
• Certificate Translation for Optimizing Compilers

Cited in

(7)

• AutoBayes/CC
• Verification of finite iterations over collections of variable data structures
• AutoBayes: a system for generating data analysis programs from statistical models
• AutoBayes/CC -- combining program synthesis with automatic code certification -- system description
• A generic software safety document generator
• Symbolic Verification Method for Definite Iterations over Tuples of Altered Data Structures and Its Application to Pointer Programs
• Automated Deduction – CADE-19

Describes a project that uses

Uses Software

• SETHEO

This page was built for publication: Synthesizing certified code

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4808844)