WG 2.11 - User contributions [en]

WG211/M11Herrmann

2012-06-03T18:08:52Z

Christoph:

I will present a new aspect of software engineering which involves the automatic
derivation of parameterised program properties during generation of low-level programs
(such as assembly code for an abstract machine) from high-level specifications (such as SQL).
For certain properties in dedicated application areas, such as worst-case
execution time for embedded systems, much effort has been spent to adapt or
instrument programs to fit the need of existing analysis tools, but this can only
assist such tools concerning aspects they are already prepared for. In industrial
settings where manual instrumentation or code adaptation would be infeasible due to
the program size, severe limitations such as constant upper bounds on loops are imposed
before carrying out a completely automatic worst-case execution time analysis.
I think that it could be very useful to derive program properties during the generation including
as many design decisions as possible, maybe interactively guided by a manual design process.
The predominant development approach in practice is to first write a program and then
to test it on concrete data, profile it and change it if it does not fit the expectations.
At the other end of the scale is the approach of using a programming language with dependent
types, which would provide even strong formal guarantees by an independent instance (the type checker)
but also slows down the program development process due to the need to find appropriate proofs at
many places. I believe that the approach of combining generation with analysis can establish both a
rapid program development and provide an analysis which benefits from design knowledge
and delivers results which are parameterised, i.e. valid for an entire range of values for
important control parameters, such as the size of the problem instance.

WG211/M11Herrmann

2012-06-03T17:48:27Z

Christoph:

I will present a new aspect of software engineering which involves the automatic
derivation of program properties during generation of low-level programs (assembly
code for an abstract machine) from high-level specifications (such as SQL).
For certain properties in dedicated application areas, such as worst-case
execution time for embedded systems, much effort has been spent to adapt or
instrument programs to fit the need of existing analysis tools, but this can only
assist such tools concerning aspects they are already prepared for.
I am convinced that efforts are better spent in developing analyses together with
the program generation or interactively with the manual design process.
The predominant development approach in practice is to first write a program and then
to profile and change it if it does not fit the expectations. At the other end of the
scale is the approach of using a programming language with dependent types, which
would provide even strong formal guarantees but also slows down the program
development process due to the need to find appropriate proofs at many places.
I believe that the approach of combining generation with analysis can unite both a
rapid program development and an analysis which benefits from design knowledge
and can provide results which are parameterised, i.e. valid for an entire range of
control parameters.

WG211/M11Herrmann

2012-06-03T17:37:41Z

Christoph: Created page with "I will present a new aspect of software engineering which involves the automatic derivation of program properties during generation of low-level programs (assembly code for an a..."

I will present a new aspect of software engineering which involves the automatic
derivation of program properties during generation of low-level programs (assembly
code for an abstract machine) from high-level specifications (such as SQL).
For certain properties in dedicated application areas, such as worst-case
execution time for embedded systems, much effort has been spent to adapt or
instrument programs to fit the need of existing analysis tools, but this can only
assist such tools concerning aspects they are already prepared for.
I am convinced that efforts are better spent in developing analyses together with
the program generation or interactively with the manual design process.
The predominant development approach in practice is first to write a program and then
to analyse and change it if it does not fit the expectations. At the other end of the
scale is the approach of using a programming language with dependent types, which
would provide even strong formal guarantees but also slows down the program
development process due to the need to find appropriate proofs at many places.
I believe that the approach of combining generation with analysis can unite both a
rapid program development and an analysis which benefits from design knowledge.

WG211/M11Schedule

2012-06-03T16:34:10Z

Christoph:

[[Category:WG211]]

=IFIP Working Group 2.11, Eleventh Meeting=
==June 25-27, 2012, Halmstad, Sweden==

===Venue and Travel===

The meeting will be held at Halmstad University in Sweden, June 25-27, hosted by Walid Taha. '''Registration and hotel booking deadline: May 7th.''' The meeting starts June 25th in the morning, and ends with a lunch on June 27th.

For accommodation, you are recommended the Hotel Mårtensson. To get a special rate of SEK 928/night including breakfast and VAT, booking '''must''' be made by either by e-mail to malin.nilsson@firsthotels.se or by phoning them, tel: +46 35 17 75 75, as this is a group arrangement. Use the booking code sent to you by email (contact [[mailto:ups@mmmi.sdu.dk Ulrik Schultz ]] if you do not have it.) To get this rate, you must book by May 7th, and you should not book through the hotel's web page (but by email, as described above). If you want more information or review other booking options, please see [http://www.firsthotels.com/Our-hotels/Hotels-in-Sweden/Halmstad/First-Hotel-Martenson/ http://www.firsthotels.com/Our-hotels/Hotels-in-Sweden/Halmstad/First-Hotel-Martenson/].

The official directions for getting to campus can be found [http://www.hh.se/english/abouttheuniversity/visitus.307_en.html here]. To simplify matters, if you are flying in internationally you might find it easiest to fly into Copenhagen (CPH) airport, which is locally known as Kastrup (as on the instructions on the above mentioned page). The best thing about flying into CPH is that you just buy a train ticket and take a train to Halmstad when you arrive. The train leaves from the airport itself. Once in Halmstad, everything is either in walking distance or a short cab ride away. Usually there are cabs at the station, but in case there are none there is a little phone that connects directly to the local taxi company.

Note that CPH is in Denmark, which is a different country. So, if you need visas for European countries, make sure you get one that works for both. If for some reason you cannot or do not want to use CPH, the next best international airport is in Gothenburg (GOT), locally known as Landvetter. The tricky thing about using that airport is that you would first have to take a 45 minute shuttle from the airport to the Gothenburg train station, and then take the train to Halmstad. That's one transfer and one wait.

===Related events===

The workshop on Reversible Computing [http://www.reversible-computation.org RC 2012] is located in Copenhagen the week after, July 2-3.

===Registration===

Registration is done using Paypal, deadline is May 7th, and the registration fee is SEK 2500. Link is available in the left-hand column on this page. Registration covers lunch, dinners, coffee breaks, and transportation for an excursion.

Please remember to either add yourself to the list of attendees or send an email to [[mailto:ups@mmmi.sdu.dk Ulrik Schultz ]]. If you are giving a talk, please either add your topic to the list below or email Ulrik.

===Attendees===

Sven Apel (Monday+Tuesday), Emilie Balland, Eric Bodden, Edwin Brady, Anthony Cleve (Monday+Tuesday), Olivier Danvy, Ewen Denney, Bernd Fischer, Robert Glueck, Gorel Hedin, Christoph Herrmann, Christian Kaestner, Julia Lawall, Christian Lengauer, Peter Mosses, John O'Donnell (talk Monday or Tuesday), Markus Puschel, Klaus Ostermann, Morten Rhiger, Ina Schaefer, Sven-Bodo Scholz, Ulrik Schultz, Tony Sloane, Jorg Striegnitz, Walid Taha, Eelco Visser, Eric van Wyk

===Talks===

If you are giving a talk, email Ulrik the title and the abstract. Alternatively, if you have access to the wiki, add it yourself following the examples below:

Talks:
* [[WG211/M11Apel | Product-Line Analysis: Experience and Prospects]] Sven Apel (Monday/Tuesday)
* [[WG211/M11Balland | Design-driven Development of Dependable Applications: A Case Study in Avionics]] Emilie Balland
* [[WG211/M11Bodden | IFDS/IDE-based Inter-procedural Static Analysis of Software Product Lines]] Eric Bodden (Monday/Tuesday)
* [[WG211/M11Brady | Implementing Domain Specific Languages by Syntax Overloading]] Edwin Brady
* [[WG211/M11Glueck | Bootstrapping compiler generators from partial evaluators]] Robert Glueck
* [[WG211/M11Herrmann | Derivation of program properties during generation]] Christoph Herrmann
* [[WG211/M11Hedin | Parameterized reference attributes: examples and properties]] Gorel Hedin
* [[WG211/M11Kaestner | Variability Mining]] Christian Kaestner
* [[WG211/M11Mosses | Component-based bisimilarity]] Peter Mosses
* [[WG211/M11ODonnell | Generating Debuggers and Fast Simulators from Functional Circuit Specifications]] John O'Donnell
* [[WG211/M11Puschel | Computer Generation of IP Cores]] Markus Puschel
* [[WG211/M11Schaefer | Incremental model-based testing of software product lines]] Ina Schaefer (Tuesday/Wednesday)
* [[WG211/M11Sloane | Profile-based Analysis and Abstraction of Attribute Evaluation]] Tony Sloane
* [[WG211/M11Visser | Declarative Language Definition (in Spoofax)]] Eelco Visser
* [[WG211/M11Schultz | Reversible Interpretation in Modular Robots]] Ulrik Schultz

Overall schedule: TBD