1. Faiez Zalila (ENSEEIHT)
Formal Verification Integration Approach for DSML
Abstract:
The application of formal methods (especially, model checking and static analysis techniques) for the verification of safety critical embedded systems has produced very good results and raised the interest of end users up to the application of these technologies in real size projects. However, these methods usually rely on specific verification oriented formal languages. It is thus mandatory to embed the associated tools in automated verification toolchains that allow users to rely on their usual business languages while enjoying the benefits of these powerful methods. Toolchains will rely on automated translation between both languages. However, the semantic gap between these languages is a very serious barrier in the specification and implementation of this translational interpretation of the business models semantics in the formal level. This problem can be handled by relying on intermediate languages. Another barrier is the interpretation of verification results from the formal level by the end users in the business world. This contribution presents some early results about methodological guidelines interpreting formal verification results as business scenarios while passing through intermediate languages.
2. Sebastian Fischer
On the Laws for Bidirectional Transformations
Abstract:
Bidirectional Transformations (BX), programs that come with an automatic way to reconstruct their input based on their output, are gaining interest in the programming language community. This community has developed laws to accompany BX for programmers to reason about transformations without knowledge of the underlying automatisms. These laws capture intuitions about BX but lack theoretical background beyond such intuitions.
We aim at developing a systematic foundation for BX by relating it to existing mathematical concepts. We investigate the connections between existing laws for BX and standard mathematical concepts, such as injectivity and surjectivity. We find that a certain class of BX is uniquely determined by their backwards transformations which suggests to let programmers specify BX by defining backwards transformations and getting forward transformations for free.
1. John Plaice (University of New South Wales)
Higher-order Multidimensional Programming
Abstract:
We present a higher-order functional language in which
variables define arbitrary-dimensional entities, where any atomic value
may be used as a dimension, and a multidimensional runtime context is
used to index the variables. We give an intuitive presentation
of the language, present the denotational semantics, and demonstrate
how function applications over these potentially infinite data structures
can be transformed into manipulations of the runtime context.
There are two kinds of functional abstraction and application: call-by-value
(eager evaluation) is used to pass dimensions and constants, while call-by-name
(lazy evaluation) is used for passing multidimensional variables.
The multidimensional space can be used for both programming and implementation
purposes. At the programming level, the informal presentation of the language
gives many examples showing the utility of describing common computing entities
as infinite multidimensional data structures.
At the implementation level, the main technical part of the talk demonstrates
that the higher-order functions over infinite data structures---even ones
that are curried---can be statically transformed into equivalent functions
directly manipulating the context, thereby avoiding the need for closures
over parts of the environment.
2. Sebastian Fischer
Generate, Test, and Aggregate: An Algebraic Method for Developing Divide-and-Conquer Algorithms
Abstract:
Divide-and-Conquer is an important algorithm design paradigm where a
problem is divided into sub-problems that can be conquered
individually. Recent opportunities to parallelize computations draw
new interest to this paradigm as individual sub-problems can be solved
in parallel. For example, the MapReduce framework allows to distribute
massively parallel computations based on associative combining
operations that leave the necessary freedom to be executed in
parallel.
Unfortunately, associative combining operations are often non-trivial
and there is little support helping programmers to define them. I will
present a method that facilitates the implementation of parallel
algorithms in divide-and-conquer style by helping programmers to
define complex associative combining operations based on more
intuitive specifications in generate-test-and-aggregate style. The
method has firm algebraic roots and functional programming will be
helpful in explaining it based on program calculation.
Back to the top page