From: Jurgen J. Vinju
To:
Date: Tue, 31 Oct 2006 14:08:52 +0100
Subject: 4-12-2006: Talk on generating programs for statistical analysis by

Dear colleagues,

You are invited to attend a talk by Bernd Fischer on program synthesis
for the statistical analysis domain, which will specifically address two 
methods for assuring reliability of the generated programs.

Date: Monday, December 4th at 10:00u
Location: CWI <room to be announced>
Titel: Assurance Techniques for Code Generators
Speaker: Bernd Fischer
Affiliation: School of Electronics and Computer Science, University of 
Southampton, UK

Abstract:
Automated code generation is an enabling technology for model-based
software development and promises many advantages but the reliability of
the generated code is still often considered as a weak point,
particularly in safety-critical domains. Traditionally,
correctness-by-construction techniques have been seen as the "right" way
to assure reliability, but these techniques remain difficult to
implement and to scale up, and have not seen widespread use. Currently,
generators are validated primarily by testing, which cannot guarantee
reliability and quickly becomes excessive.

In this talk, we present two related alternative assurance approaches
that use Hoare-style safety proofs to ensure that the generated code
does not "go wrong", i.e., does not violate specific safety conditions
during its execution.  The first approach is based on the insight that
code generator itself can be extended to produce all annotations (i.e.,
pre-/postconditions and loop invariants) required to enable the safety
proofs for each individual generated program, without compromising the
assurance provided by the subsequent verification phase. The second
approach is based on the insight that the output of a code generator is
highly idiomatic, so that we can use patterns to describe all code
constructs that require annotations and templates to describe the
required annotations. We use techniques similar to aspect-oriented
programming to add the annotations to the generated code: the patterns
correspond to (static) point-cut descriptors, while the introduced
annotations correspond to advice.

We have implemented these approaches in the AutoBayes and AutoFilter
code generators and used it to fully automatically prove that the
generated code satisfies both language-specific properties such as
array-bounds safety or proper variable initialization-before-use and
domain-specific properties such as vector normalization, matrix
symmetry, or correct sensor input usage.

Joint work with Ewen Denney, USRA/RIACS, NASA Ames Research Center, USA.

[AutoBayes/AutoFilter is a fully automatic program synthesis system for
the statistical data analysis domain. Its input is a concise description
of a data analysis problem in the form of a statistical model; its
output is optimized and fully documented C/C++ code which can be linked
dynamically into the Matlab and Octave environments.]