Workshops and Tutorials
Workshop dates: 10-11 June 2013.
The 4th International Workshop on Computational Models for Cell Processes (CompMod 2013)Organisers:
Computational systems biology is an exciting new application area for applied mathematics and computer science. This workshop of the 10th International Conference on integrated Formal Methods (iFM) fosters an excellent platform gathering researchers in formal methods and related fields that are interested in the wealth of opportunities and challenges in systems biology.
Rodin User and Developer Workshop 2013Website: http://wiki.event-b.org/index.php/Rodin_Workshop_2013
Event-B is a formal method for system-level modelling and analysis. The Rodin Platform is an Eclipse-based toolset for Event-B that provides effective support for modelling and automated proof. The platform is open source and is further extendable with plug-ins. A range of plug-ins have already been developed including ones that support animation, model checking and UML-B. While much of the development and use of Rodin takes place within EU FP7 Projects (RODIN, DEPLOY, ADVANCE), there is a growing group of users and plug-in developers outside these projects. The purpose of this workshop is to bring together existing and potential users and developers of the Rodin toolset and to foster a broader community of Rodin users and developers.
BCS FACS 2013 Refinement Workshop 2013Website: http://www.refinenet.org.uk/ref13/cfp.html
Refinement is one of the cornerstones of a formal approach to software engineering: the process of developing a more detailed design or implementation from an abstract specification through a sequence of mathematically-based steps that maintain correctness with respect to the original specification. The aim of this BCS FACS Refinement Workshop, is to bring together people who are interested in the development of more concrete designs or executable programs from abstract specifications using formal notations, tool support for formal software development, and practical experience with formal refinement methodologies.
Tutorial: Specification and Proof of Programs with Frama-COrganisers:
Despite the spectacular progress made by the developers of formal verification tools, their usage remains basically reserved for the most critical software. More and more engineers and researchers today are interested in such tools in order to integrate them into their everyday work. This half-day tutorial proposes a practical introduction during which the participants will write C program specifications, observe the proof results, analyze proof failures and fix them. Participants will be taught how to write a specification for a C program, in the form of function contracts, and easily prove it with an automatic tool in FRAMA-C, a freely available software
verification toolset. Those who will have FRAMA-C and JESSIE installed (e.g. from ready-to-install packages frama-c, why, alt-ergo under Linux) will also run automatic proof of
programs on their computer. Program specifications will be written in the specification language ACSL similar to other specification languages like JML that some participants may know. ACSL-syntax is intentionally close to C and can be easily learned on-the-fly.
12:30 - 13:30: Lunch
13.30 - 14:15: Presentation of the Frama-C platform
14:15 - 15:15: Basic specification and verification with WP plug-in
15:15 - 15:45: Coffee break
15:45 - 16:30: Loop invariant and variant
16:30 - 17:30: Advanced specification and verification
Material from the tutorial can be found at: http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:tutorial:ifm-2013
The Overture and FMDEP workshops have been cancelled!
|Email: email@example.com, Phone: +358-2-2154475, Fax: +358-2-2515557|