Synthesizing Certified Code
- 9 July 2002
- book chapter
- Published by Springer Nature
- p. 431-450
- https://doi.org/10.1007/3-540-45614-7_25
Abstract
No abstract availableKeywords
This publication has 23 references indexed in Scilit:
- AutoBayes: a system for generating data analysis programs from statistical modelsJournal of Functional Programming, 2003
- Dynamically discovering likely program invariants to support program evolutionIEEE Transactions on Software Engineering, 2001
- A certifying compiler for JavaACM SIGPLAN Notices, 2000
- Eliminating array bound checking through dependent typesACM SIGPLAN Notices, 1998
- Program SynthesisPublished by Springer Nature ,1998
- Supporting contexts in program refinementScience of Computer Programming, 1997
- The Kiv-approach to software verificationPublished by Springer Nature ,1995
- SETHEO: A high-performance theorem proverJournal of Automated Reasoning, 1992
- A logic covering undefinedness in program proofsActa Informatica, 1984
- Verification of Array, Record, and Pointer Operations in PascalACM Transactions on Programming Languages and Systems, 1979