Rich Model Toolkit COST Action Meeting, 16-17 June 2013

The workshop will be held in the Corinthia Palace Hotel, De Paule Avenue, San Anton. Participants will get special room rates - more information can be found in the Local Arrangements section.

The workshop is being coordinated by the University of Malta. The Malta Council for Science and Technology (MCST) is the managing authority for COST in Malta.

The planned structure of the workshop will be filled in with more detail closer to the date.

Meeting is organized by Gordon Pace and Cesar Sanchez.

This workshop serves as the meeting of the Rich Model Toolkit COST Action IC0901. Information about the Action: http://richmodels.epfl.ch/

The meeting continues a series of meetings held in Brussels, Belgrade, Edinburgh, Lugano, Saarbruecken, Dagstuhl, Turin, Tallinn, Trento, Manchester, Haifa and Rome held in the period 2009-2013.

Accommodation

The workshop will be held at the Corinthia Palace Hotel (5*), De Paule Avenue, San Anton, with which special accommodation rates have been arranged for participants. The hotel is poised midway between Malta’s capital Valletta, and the so-called ‘silent’ city of Mdina, and across the road from the 17th century San Anton Presidential Palace. The Corinthia Palace Hotel & Spa was originally built in the 19th century as a luxury private villa, the grand design and immaculately-landscaped gardens have inspired guests from around the world.

Deluxe garden-view room on bed & breakfast basis is at 90 euros per night (for sole use). Second person supplement is 20 euros per night.

Participants are requested to email Lorraine Dunnett (lorraine.dunnett@corinthia.com) and Alex Cardona (alex.cardona@corinthia.com) for bookings. You are encouraged to book till 1st May, until when the hotel will be blocking a number of rooms - after this date it will be on a first come first served basis.

Workshop Dinner

A workshop dinner will be held at Palazzo de Piro at 36 euros (including transport) on Sunday 16th June. Palazzo de Piro is a 17th Century Palazzo nestled in the bastion walls of the medieval city of Mdina, Malta’s Silent City. The existing structure was originally three separate houses, the oldest parts of which date back to the second half of the 16th century. The emblem on the main entrance hall indicates they were built by Malta’s most famous architect Girolamo Cassar.

Local Organisation Matters

If you have any questions regarding logistics you can email directly Ms Lucienne Bugeja (conferences@um.edu.mt).

We are pleased to confirm keynotes from:

• John Gallagher (Roskilde University, DK and IMDEA Software, Spain)
• Manuel Hermenegildo (IMDEA Software, Spain)

Researchers have developed a number of useful tools for automated analysis of particular classes of models of computer systems:

• software vendors are using static analyses supported by automated theorem provers and constraint solvers to prevent software crashes;
• hardware manufacturers are using SAT solvers,model checkers, and theorem provers to identify and correct errors that could have enormous financial consequences;
• description logic reasoners analyze relationships between tens of thousands of terms in medical ontologies and verify their consistency;
• aircraft manufacturers and space agencies are using analysis tools based on abstract interpretation to eliminate errors in aircraft control software.

Despite these successes, today’s automated analysis methods are not widespread in engineering practice. Among the factors contributing to this state of affairs are the limitations of the tools themselves: insufficient automation, specialized input formats, and no support for high-level synthesis. Another factor is the lack of standards of quality that would easy tool interoperability and give formally certified computer system a competitive advantage over systems without formal assurance guarantees.

• Standardization of expressive languages. Formats to represent systems, formulas, proofs, counterexamples. Translation between specification languages. Benchmarks and competitions for automated reasoning, verification, analysis, synthesis.
• Decision procedures: Decision procedures for new classes of constraints. SAT and SMT implementation and certification. Encoding synthesis and analysis problems into SMT. Description logics and scalable reasoning about knowledge bases.
• Transition system analysis: Abstraction-based approaches and refinement for verification of infinite-state systems. Constraint-based program analysis. Data-flow analysis for complex domains. Extracting transition systems from programming languages and bytecodes.
• High-level synthesis: New algorithms for synthesis from high-level specifications. Extending decision procedures to perform synthesis tasks. Connections between invariant generation and code synthesis.