1. Faiez Zalila (ENSEEIHT)
Formal Verification Integration Approach for DSML
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
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
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
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.