AutoBayes/CC -- combining program synthesis with automatic code certification -- system description. 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
Keywords for this software
References in zbMATH (referenced in 3 articles , 2 standard articles )
Showing results 1 to 3 of 3.
- Denney, Ewen; Fischer, Bernd; Schumann, Johann: Using automated theorem provers to certify auto-generated aerospace software (2004)
- Whalen, Michael; Schumann, Johann; Fischer, Bernd: Synthesizing certified code (2002)
- Whalen, Michael; Schumann, Johann; Fischer, Bernd: AutoBayes/CC -- combining program synthesis with automatic code certification -- system description (2002)