|
|
 |
|
Formal Methods Seminar by Ewen Denney |
|
Date: July 25, 2005
Time: 10:30am
Location: NIA, Rm 137
Additional Information: Presentation (PDF)
Certifiable Program Synthesis
Ewen Denney, NASA Ames Research Center
Automated code generation is a technology which could be applied in many NASA missions but concerns over the safety, comprehensibility, and adaptability of generated code hamper its widespread adoption. One solution to the safety problem is to extend the generator in such a way that it automatically certifies that the code it generates is safe, a technique we call certifiable program synthesis. I will describe the domain-specific code generators, AutoBayes and AutoFilter, which work in the domains of data analysis and state estimation, respectively, and give an overview of some of the techniques we use to achieve safety.
|
|
|
Home