University of Minnesota
Software Engineering Center
/

You are here

Johann Schumann

Recent Publications

Certification Support for Automatically Generated Programs

Although autocoding techniques promise large gains in software development productivity, their "real-world" application has been limited, particularly in safety-critical domains. Often, the major impediment is the missing trustworthiness of these systems: demonstrating — let alone formally certifying — the trustworthiness of automatic code generators is extremely difficult due to their complexity and size.

Certifying Synthesized Code

Code certication is a lightweight approach for formally demonstrating software quality. Its basic idea is to require code producers to provide formal proofs that their code satises certain quality properties. These proofs serve as certicates that can be checked independently. Since code certication uses the same underlying technology as program verication, it requires detailed annotations (e.g., loop invariants) to make the proofs possible. However, manually adding annotations to the code is time-consuming and error-prone.

AutoBayes/CC – Combining Program Synthesis with Automatic Code Certification

Code certication is a lightweight approach to formally demonstrate software quality. It concentrates on aspects of software quality that can be dened 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 satises these quality properties. The proofs serve as certicates which can be checked independently, by the code consumer or by certication authorities, e.g., the FAA. It is the idea underlying such approaches as proof-carrying code.