Invited Speakers

12th International Conference on integrated Formal Methods

Dimensions of Model Transformation Reuse

Marsha Chechik (University of Toronto, Canada)

Model Transformations have been called the “heart and soul” of Model-Driven software development. However, they take a lot of effort to build, verify, analyze, and debug. It is thus imperative to develop good reuse strategies that address issues specific to model transformations. In this paper, we present five transformation reuse strategies: lifting, mapping, subtyping, templating and aggregating.

Lifting a transformation reuses it for aggregate representations of models, such as product lines. Mapping a transformation designed for single models reuses it for model collections, such as megamodels. 

Subtyping is a way to reuse a transformation for different - but similar - input modelling languages. Templating brings the power of generic programming to model transformations, allowing them to be parameterized and reused for different model types. Aggregating reuses both transformation fragments (during transformation creation) and partial execution results (during transformation execution) across multiple transformations. We illustrate each of these techniques on a concrete example and discuss their strengths and weaknesses.

Symbolic Computation and Automated Reasoning for Program Analysis

Laura Kovács (Chalmers University of Technology, Sweden)

In this talk I describe how a combination of symbolic computation techniques with first-order theorem proving can be used for solving some challenges of automating program analysis, in particular for generating and proving properties about the logically complex parts of software. I will first present how computer algebra methods, such as Groebner basis computation, quantifier elimination and algebraic recurrence solving, help us in inferring properties of program loops with non-trivial arithmetic. Typical properties inferred by our work are loop invariants and expressions bounding the number of loop iterations.  I will then further extend our work to generate first-order properties of programs with unbounded data structures, such as arrays. For doing so, I will use saturation-based first-order theorem proving and extend first-order provers with support for  program analysis. Since program analysis requires reasoning in the combination of first-order theories of data structures, I will also discuss new features in first-order theorem proving, such as inductive reasoning and built-in boolean sort. These extensions allow us to express program properties directly in first-order logic and hence use further first-order theorem provers to reason about program properties.

Can Formal Methods Improve the Efficiency of Code Reviews?

Reiner Hähnle (Technical University Darmstadt, Germany)

Code reviews are a provenly effective technique to find defects in source code as well as to increase its quality.  Therefore, industrial software production often relies on code reviews as a standard QA mechanism. But, surprisingly, tool support for reviewing activities is rare. Systems like Gerrit help to keep track of the discussion during the review, but do not support the reviewing activity directly. In this paper we argue that such support can be provided by formal analysis tools and we give an empirical justification for this claim. Specifically, we use symbolic execution to improve the program understanding subtask during a code review.  Tool support is realized by an Eclipse plug-in called Symbolic Execution Debugger. It allows to explore visually a symbolic execution tree for given source code. For evaluation we carefully designed a controlled experiment where users were given various code examples that had to be inspected with and without having a symbolic execution tree available. We provide statistical evidence that with the help of symbolic execution defects are identified in a more effective manner than with a merely code-based view. Our work suggests that there is huge potential for formal methods not only in the production of safety-critical systems, but for any kind of software and as part of a standard development process.