Between Dec 19, 2024 and Jan 2, 2025, datasets can be submitted to DRUM but will not be processed until after the break. Staff will not be available to answer email during this period, and will not be able to provide DOIs until after Jan 2. If you are in need of a DOI during this period, consider Dryad or OpenICPSR. Submission responses to the UDC may also be delayed during this time.

Browsing by Author "Schumann, Johann"

Now showing 1 - 3 of 3
  • Thumbnail Image
    Item
    AutoBayes/CC – Combining Program Synthesis with Automatic Code Certification
    (Springer-Verlag, 2002) Whalen, Michael; Fischer, Bernd; Schumann, Johann
    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. Code certication can be viewed as a more practical version of traditional Hoare-style program verication. The properties to be veried are fairly simple and regular so that it is often possible to use an automated theorem prover to automatically discharge all emerging proof obligations. Usually, however, the programmer must still splice auxiliary annotations (e.g., loop invariants) into the program to facilitate the proofs. For complex properties or larger programs this quickly becomes the limiting factor for the applicability of current certication approaches. Our work combines code certication with automatic program synthesis which makes it possible to automatically generate both the code and all necessary annotations for fully automatic certication. By generating detailed annotations, one of the biggest obstacles for code certication is removed and it becomes possible to automatically check that synthesized programs obey the desired safety properties.
  • Thumbnail Image
    Item
    Certification Support for Automatically Generated Programs
    (IEEE Computer Society, 2003) Schumann, Johann; Fischer, Bernd; Whalen, Michael
    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. We develop an alternative product-oriented certification approach which is based on five principles: (1) trustworthiness of the generator is reduced to the safety of each individual generated program; (2) program safety is defined as adherence to an explicitly formulated safety policy; (3) the safety policy is formalized by a collection of logical program properties; (4) Hoare-style program verification is used to show that each generated program satisfies the required properties; (5) the code generator itself is extended to automatically produce the code annotations required for verification. The approach is feasible because the code generator has full knowledge about the program under construction and about the properties to be verified. It can thus generate all auxiliary code annotations a theorem prover needs to discharge all emerging verification obligations fully automatically. Here we report how this approach is used in a certification extension for AUTOBAYES, an automatic program synthesis system which generates data analysis programs (e.g., for clustering and time-series analysis) from declarative specifications. In particular, we describe how a variable-initialization-before-use safety policy can be encoded and certified.
  • Thumbnail Image
    Item
    Certifying Synthesized Code
    (Springer-Verlag, 2002) Whalen, Michael; Fischer, Bernd; Schumann, Johann
    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. We address this problem by combining code certication with automatic program synthesis. Given a high-level specication, our approach simultaneously generates code and all annotations required to certify the generated code. We describe a certication extension of AutoBayes, a synthesis tool for automatically generating data analysis programs. Based on built-in domain knowledge, proof annotations are added and used to generate proof obligations that are discharged by the automated theorem prover E-SETHEO. We demonstrate our approach by certifying operator- and memory-safety on a data-classication program. For this program, our approach was faster and more precise than PolySpace, a commercial static analysis tool.