[ecoop-info] it-fmeurope-events Digest Tue, 04 Jul 2017
it-fmeurope-events-request at lists.uu.se
it-fmeurope-events-request at lists.uu.se
Tue Jul 4 19:15:18 CEST 2017
it-fmeurope-events digest Tue, 04 Jul 2017
Table of contents:
* 1 - [FME Events] CFP IMPEX2017 : First International Workshop on Handling
IMPlicit and EXplicit knowledge in formal system development. - mery
<dominique.mery at loria.fr>
* 2 - [FME Events] [fm-announcements] RV-CuBES Deadline Extension - "Havelund,
Klaus (348B)" <Klaus.Havelund at jpl.nasa.gov>
* 3 - [FME Events] RV-CuBES Deadline Extension - Klaus Havelund
<compscience.announcement at gmail.com>
* 4 - [FME Events] [iFM'17] Call for Participation for the International
Conference on integrated Formal Methods 2017 - Ingrid Chieh Yu
<ingridcy at ifi.uio.no>
----------------------------------------------------------------------
Message-ID: <b24f3082-e12b-f731-0412-e8df967be0fe at loria.fr>
Date: Sat, 1 Jul 2017 22:28:29 +0200
From: mery <dominique.mery at loria.fr>
Subject: [FME Events] CFP IMPEX2017 : First International Workshop on Handling
IMPlicit and EXplicit knowledge in formal system development.
================================================================================================
CALL FOR PAPERS
IMPEX 2017
First International Workshop on Handling IMPlicit and
EXplicit knowledge in formal system development.
Co-located with ICFEM 2017
Xi'an, China, 13-17th November 2017
================================================================================================
*Background and Objectives*
Most of methods based on proof systems, such as theorem provers, model
checkers or any reasoning systems, rely on the definition and use of
basic theories (logic, algebraic, types, etc.) in order to support the
expression of proofs in formal developments. They also propose
mechanisms and operators to define new theories (inside contexts or
theories or species, like in Event-B, COQ, Isabelle/HOL, FOCAL, Nuprl,
ASM, PVS, etc.) or to enrich their basic theories. In general, the
definition of a theory is based on mathematical and logical abstract
concepts that support the formalisation of the studied hardware and/or
software systems. In other words, the semantics of such formalised
systems is expressed in this theory; i.e. the used theory gives the
semantics of all the systems formalised in this theory and the
required properties of these systems are expressed and checked in the
same theory. This kind of semantics represents the implicit
semantics. Note that the same semantics is used for a wide variety of
heterogeneous hardware and/or software systems.
Generally, hardware and/or software systems are associated to
information issued from the application domain in which they
evolve. For example, one integer variable (typed by an integer in the
theory) may denote a temperature expressed in Celsius degrees, whilst
another one may denote a pressure measured in bars at the extreme
limit of the left wing of an aircraft in the landing phase. In
general, this kind of knowledge is omitted by the produced
formalisations or their formalisation is hardcoded in the designed
formal model. If this knowledge carried by the concepts manipulated in
these formal models is still in the mind of the model designer, it is
not explicitly formalised and therefore, it is not shared in the same
way as for implicit theories that can be reused in several formal
developments. This kind of knowledge represents the explicit
semantics.
The objective of the meeting is to discuss on mechanisms for reducing
heterogeneity of models induced by the absence of explicit semantics
expression in the formal techniques used to specify these models. More
precisely, the meeting targets to highlight the advances in handling
both implicit and explicit semantics in formal system developments.
*List of Topics*
Discussions, presentations and more generally, contributions
shalladdress one or more topics described below
Show that when making explicit the domain knowledge in formal
models, several relevant hidden (because they are not
explicitlymodelled in classical formal modelling languages) properties
can be handled
How knowledge models, like ontologies, can be handled in formal
system developments?
What are the candidate formal modelling languages and techniques
to model such domain knowledge? What are the reasoning capabilities
entailed by these modelling languages?
Define relevant case studies that illustrate the need to
make explicit domain properties?
Define composition mechanisms to handle domain knowledge in
formal modelling techniques. Beyond the technical results targeted
by the proposed meeting, social, economic and resilience impacts
are expected. These impacts are built on the foundations of
heterogeneity reduction and formal model alignment.
Submission Guidelines
Papers should be written in English and not exceed 15 pages for long
papers and 8 pages for short papers in EPTCS format
(http://http//www.eptcs.org/ for details). Submission should be made
through the IMPEX 2017 submission page
(https://easychair.org/conferences/?conf=impex2017), handled by the
EasyChair conference management system.
Important Dates
Abstract Submission: 26 August 2017
Full Paper Submission: 2 September 2017
Acceptance/Rejection Notification: 1 October 2017
Camera-ready Paper: 30 November 2017
Program Committee
Yamine Ait Ameur, IRIT/INPT-ENSEEIHT, France
Marco Casanova, Catholic University of Rio de Janeiro, Brazil
Calvanese Diego, Free University of Bozen-Bolzano, Italy
Eric Dubois, Luxembourg Institute for Science and Technology,
Luxembourg
Josﾃｩ Fiadeiro, University of Leicester, UK
Marc Frappier, University of Sherbrooke, Canada
Stefania Gnesi, ISTI-CNR, Italy
Thai Son Hoang, University of Southampton, UK
Fuyuki Ishikawa, National Institute of Informatics, Japan
Régine Laleau, LACL, University of Paris-Est Crﾃｩteil, France
(co-chair)
Dominique Méry, LORIA, University of Lorraine, France (co-chair)
Shin Nakajima, National Institute of Informatics, Japan (co-chair)
John Rushby, SRI International, California, USA
Klaus-Dieter Schewe, Software Competence Centre Hagenberg, Linz,
Austria
Cong Tian, Xidian University, China
Elena Troubitsyna, ｜o Akademi University, Finland
Qing Wang, Australian National University, Canberra, Australia
Alan Wassyng, McMaster University, Canada
Hirokazu Yatsu, Kyushu University, Fukuoka, Japan
Organizing committee
Régine Laleau, LACL, University of Paris-Est Crﾃｩteil, France
Dominique Méry, LORIA, University of Lorraine, France
Shin Nakajima, National Institute of Informatics, Japan
Publication
Papers accepted for presentation are planned to be published in EPTCS
(under request to editor). Authors of selected papers from IMPEX 2017
will be invited to submit an extended version to a journal (ISSE
Springer agreement). However, such an invitation does not imply
acceptance of the paper. All the submissions will be evaluated
following the guidelines set by the journal. Only those which
satisfy all the criteria will be accepted for publication.
All questions about submissions should be emailed to Régine Laleau or
Dominique Méry or Shin Nakajima
Sponsors
------------------------------
Message-ID: <D57C7C0F.1D98F%klaus.havelund at jpl.nasa.gov>
Date: Sat, 1 Jul 2017 05:07:15 +0000
From: "Havelund, Klaus (348B)" <Klaus.Havelund at jpl.nasa.gov>
Subject: [FME Events] [fm-announcements] RV-CuBES Deadline Extension
RV-CuBES
An International Workshop on Competitions, Usability, Benchmarks, Evaluation,
and Standardisation for Runtime Verification Tools
Held in conjunction with the 17th International Conference on Runtime
Verification (RV 2017)
http://rv2017.cs.manchester.ac.uk/rv-cubes/
The goal of this workshop is to provide a venue to discuss ongoing efforts to
improve how we evaluate and compare tools for runtime verification. This
workshop invites submissions that contribute to this discussion (see below).
The workshop replaces the Runtime Verification Competition this year, giving
an opportunity for reflection and planning for the future.
HIGHLIGHTS
* We invite two kinds of submissions: tool overview papers of existing
tools and position papers
* Attendance at the workshop is not compulsory for submission, but
encouraged
* The workshop will be integrated into RV 2017 to engage with the wider RV
community
BACKGROUND
Over the last three years, beginning in 2014, the Competition on Runtime
Verification (CRV) has compared 14 different runtime verification tools using
over 100 different benchmarks. It has motivated the development of new tools
and extensions of existing ones. Thanks to the time and effort of the various
organisers and participants it has successfully provided a platform to discuss
how we evaluate and compare our tools. However, we are aware that the
competition has not served all members of the community and required
significant effort from its participants and therefore we have decided not to
run the competition in the same form in 2017.
This workshop has two aims.
* Firstly, to kickstart an online repository of tool descriptions that
focus on usability, rather than implementation. Much effort within Runtime
Verification is spent developing tools. The planned repository will help
advertise these tools within and beyond the community and to document their
existence. To this end, this workshop invites tool overview papers (details
below) that present an opportunity to demonstrate the diverse range of
available RV tools and to advertise their advanced features and capabilities.
* Secondly, to provide a forum in which the future of the competition, and
wider efforts to improve how we evaluate RV tools, can be discussed in a
structured and informed way. There have been various informal discussions at
the previous three RV conferences and in other settings. By inviting position
papers (details below) this workshop aims to establish the issues and possible
directions before holding a structured panel session during RV 2017.
RELATION TO RV 2017
There is no overlap in scope between this workshop and RV 2017. Any papers
containing original technical developments should be submitted to RV 2017
rather than this workshop as the workshop focuses on tool reviews (containing
existing work) and position statements. If there is any uncertainty please
contact the workshop chairs.
The workshop will be integrated into RV 2017. The workshop activities will
include a poster presentation session and a panel decision, both of which will
be scheduled within the main conference program. A consequence of this is that
there will be no separate registration for the workshop. To attend the
workshop activities it will be necessary to attend RV 2017. Although,
attendance is not a requirement for submission.
SUBMISSIONS
We invite two forms of submission: Tool Overview papers and Position papers.
All submissions will be subject to a lightweight review by the PC to ensure a
reasonable standard and to provide constructive feedback to improve the
quality of the submission.
Tool Overview Papers
These should describe an existing tool using a minimum of 5 pages. The paper
should at least describe how to obtain the tool, the RV problem the tool is
aiming to solve, the key defining features of the tool and relevant
references. Additionally, we might expect it to include some of the following:
* The history of the tool
* High-level overviews of key aspect such as the input language or
architecture from a user’s perspective
* Usability details undocumented elsewhere
* Examples demonstrating key features
* Details of case studies or applications to real world problems
* Discussion of features particular to the tool
* Summaries (rather than detailed tables) of experimental results
* Analysis of the kinds of problem the tool is suited for and those it is
less-well suited for
Ideally, the tool and related material (e.g. benchmarks) will be available
online and linked to in the submission. The paper should not cover any
significant new contributions (these can be submitted as tool papers to RV
2017) and should rely on previous research and tool papers to provide further
details. Note that there is no upper page limit however the number of pages
used should reflect the level of detail given. Submissions of 2 pages giving
minimal details would be suitable in a situation where the tool is well
documented elsewhere but an entry in the repository is still desired. All
accepted submissions will be invited for presentation at a special Poster
session during RV 2017.
Position papers
Initial submissions should use a minimum of 2 pages to explore a particular
position related to the evaluation, comparison or standardisation of Runtime
Verification tools (and benchmarks). Topics may include, but are not limited
to:
* What should a RV benchmark look like?
* Can we have a common specification language for RV? If so, what should
it look like?
* Is execution time the most important performance criteria? What might be
more important?
* How can we evaluate hardware monitoring tools?
* What are we doing wrong in evaluation? Can we fix this?
* What can be borrowed form other communities?
A selection of position papers will be used to structure a discussion panel to
be held at RV 2017. Again, there is no upper page limit however the number of
pages used should reflect the level of detail given. There will be an
opportunity to update the paper based on discussions before inclusion in post-
proceedings (see below).
Publishing and Submission
Contributions will be published as a post-proceedings volume in the Open-
Access Scopus-Indexed EasyChair Kalpa
<http://www.easychair.org/publications/Kalpa> Series. To be eligible for
inclusion in the post-proceedings, papers should be at least 5 pages. Please
see the relevant information for
authors<http://www.easychair.org/publications/for_authors> when preparing your
paper.
Please submit contributions to the following EasyChair page.
https://easychair.org/conferences/?conf=rvcubes2017
DATES
* Submission Deadline 1 July 2017
* Abstracts: 8 July 2017
* Final Submission: 15 July 2017
* Notification 1 August 2017
* Workshop at RV 2017 13-16 September 2017
* Post-proceedings deadline 14 October 2017
ORGANISATION
For local and general organisation please see RV 2017.
Program Committee Chairs
Giles Reger, University of Manchester, UK
Klaus Havelund, NASA Jet Propulsion Laboratory, USA
Program Committee
Ezio Bartocci, TU Wien, Austria
Domenico Bianculli, SnT Centre – University of Luxembourg, Luxembourg
Borzoo Bonakdarpour, McMaster University, Cananda
Christian Colombo, University of Malta, Malta
Ylies Falcone, Univ. Grenoble Alpes, Inria, Laboratoire d’Informatique de
Grenoble, France
Adrian Francalanza, University of Malta, Malta
Sylvain Hallé, Université du Québec à Chicoutimi, Canada
Felix Klaedtke, NEC Europe Ltd.
Daniel Thoma, University of Lübeck, Germany
Dmitriy Traytel, ETH Zürich, Switzerland
Gordon Pace, University of Malta, Malta
Cesar Sanchez, IMDEA Software Institute, Spain
Leonardo Mariani, University of Milano Bicocca, Italy
Julien Signoles, CEA LIST, France
Tarmo Uustalu, Tallin University of Technology, Estonia
---
To opt-out from this mailing list, send an email to
fm-announcements-request at lists.nasa.gov
with the word 'unsubscribe' as subject or in the body. You can also make the
request by contacting
fm-announcements-owner at lists.nasa.gov
------------------------------
Message-ID:
<CABdH3mC4MrkvLHUgiKG0qnWWsNyUb8BqJAbe5TNXxB3wyCSM5A at mail.gmail.com>
Date: Fri, 30 Jun 2017 22:11:15 -0700
From: Klaus Havelund <compscience.announcement at gmail.com>
Subject: [FME Events] RV-CuBES Deadline Extension
RV-CuBESAn International Workshop on Competitions, Usability, Benchmarks,
Evaluation, and Standardisation for Runtime Verification ToolsHeld in
conjunction with the 17th International Conference on Runtime Verification
(RV 2017)
http://rv2017.cs.manchester.ac.uk/rv-cubes/
The goal of this workshop is to provide a venue to discuss ongoing efforts
to improve how we evaluate and compare tools for runtime verification. This
workshop invites submissions that contribute to this discussion (see
below). The workshop replaces the Runtime Verification Competition this
year, giving an opportunity for reflection and planning for the future.
*HIGHLIGHTS*
- We invite two kinds of submissions: tool overview papers of
*existing* tools
and position papers
- Attendance at the workshop *is not compulsory* for submission, but
encouraged
- The workshop will be integrated into RV 2017 to engage with the wider
RV community
*BACKGROUND*
Over the last three years, beginning in 2014, the Competition on Runtime
Verification (CRV) has compared 14 different runtime verification tools
using over 100 different benchmarks. It has motivated the development of
new tools and extensions of existing ones. Thanks to the time and effort of
the various organisers and participants it has successfully provided a
platform to discuss how we evaluate and compare our tools. However, we are
aware that the competition has not served all members of the community and
required significant effort from its participants and therefore we have
decided not to run the competition in the same form in 2017.
This workshop has two aims.
- Firstly, to kickstart an online repository of tool descriptions that
focus on usability, rather than implementation. Much effort within Runtime
Verification is spent developing tools. The planned repository will help
advertise these tools within and beyond the community and to document their
existence. To this end, this workshop invites tool overview papers (details
below) that present an opportunity to demonstrate the diverse range of
available RV tools and to advertise their advanced features and
capabilities.
- Secondly, to provide a forum in which the future of the competition,
and wider efforts to improve how we evaluate RV tools, can be discussed in
a structured and informed way. There have been various informal discussions
at the previous three RV conferences and in other settings. By inviting
position papers (details below) this workshop aims to establish the issues
and possible directions before holding a structured panel session during RV
2017.
*RELATION TO RV 2017*
There is no overlap in scope between this workshop and RV 2017. Any papers
containing original technical developments should be submitted to RV 2017
rather than this workshop as the workshop focuses on tool reviews
(containing existing work) and position statements. If there is any
uncertainty please contact the workshop chairs.
The workshop will be integrated into RV 2017. The workshop activities will
include a poster presentation session and a panel decision, both of which
will be scheduled within the main conference program. A consequence of this
is that there will be no separate registration for the workshop. To attend
the workshop activities it will be necessary to attend RV 2017. Although,
attendance is not a requirement for submission.
*SUBMISSIONS*
We invite two forms of submission: Tool Overview papers and Position
papers. All submissions will be subject to a lightweight review by the PC
to ensure a reasonable standard and to provide constructive feedback to
improve the quality of the submission.
*Tool Overview Papers*
These should describe an existing tool using a minimum of 5 pages. The
paper should at least describe how to obtain the tool, the RV problem the
tool is aiming to solve, the key defining features of the tool and relevant
references. Additionally, we might expect it to include some of the
following:
- The history of the tool
- High-level overviews of key aspect such as the input language or
architecture from a user’s perspective
- Usability details undocumented elsewhere
- Examples demonstrating key features
- Details of case studies or applications to real world problems
- Discussion of features particular to the tool
- Summaries (rather than detailed tables) of experimental results
- Analysis of the kinds of problem the tool is suited for and those it
is less-well suited for
Ideally, the tool and related material (e.g. benchmarks) will be available
online and linked to in the submission. The paper should not cover any
significant new contributions (these can be submitted as tool papers to RV
2017) and should rely on previous research and tool papers to provide
further details. Note that there is no upper page limit however the number
of pages used should reflect the level of detail given. Submissions of 2
pages giving minimal details would be suitable in a situation where the
tool is well documented elsewhere but an entry in the repository is still
desired. All accepted submissions will be invited for presentation at a
special Poster session during RV 2017.
*Position papers*
Initial submissions should use a minimum of 2 pages to explore a particular
position related to the evaluation, comparison or standardisation of
Runtime Verification tools (and benchmarks). Topics may include, but are
not limited to:
- What should a RV benchmark look like?
- Can we have a common specification language for RV? If so, what should
it look like?
- Is execution time the most important performance criteria? What might
be more important?
- How can we evaluate hardware monitoring tools?
- What are we doing wrong in evaluation? Can we fix this?
- What can be borrowed form other communities?
A selection of position papers will be used to structure a discussion panel
to be held at RV 2017. Again, there is no upper page limit however the
number of pages used should reflect the level of detail given. There will
be an opportunity to update the paper based on discussions before inclusion
in post-proceedings (see below).
*Publishing and Submission*
Contributions will be published as a post-proceedings volume in the
Open-Access Scopus-Indexed EasyChair Kalpa
<http://www.easychair.org/publications/Kalpa>Series. To be eligible for
inclusion in the post-proceedings, papers should be at least 5 pages.
Please see the relevant information for authors
<http://www.easychair.org/publications/for_authors> when preparing your
paper.
Please submit contributions to the following EasyChair page.
https://easychair.org/conferences/?conf=rvcubes2017
*DATES*
- Submission Deadline 1 July 2017
- Abstracts: 8 July 2017
- Final Submission: 15 July 2017
- Notification 1 August 2017
- Workshop at RV 2017 13-16 September 2017
- Post-proceedings deadline 14 October 2017
*ORGANISATION*
For local and general organisation please see RV 2017.
*Program Committee Chairs*
Giles Reger, University of Manchester, UK
Klaus Havelund, NASA Jet Propulsion Laboratory, USA
*Program Committee*
Ezio Bartocci, TU Wien, Austria
Domenico Bianculli, SnT Centre – University of Luxembourg, Luxembourg
Borzoo Bonakdarpour, McMaster University, Cananda
Christian Colombo, University of Malta, Malta
Ylies Falcone, Univ. Grenoble Alpes, Inria, Laboratoire d’Informatique de
Grenoble, France
Adrian Francalanza, University of Malta, Malta
Sylvain Hallé, Université du Québec à Chicoutimi, Canada
Felix Klaedtke, NEC Europe Ltd.
Daniel Thoma, University of Lübeck, Germany
Dmitriy Traytel, ETH Zürich, Switzerland
Gordon Pace, University of Malta, Malta
Cesar Sanchez, IMDEA Software Institute, Spain
Leonardo Mariani, University of Milano Bicocca, Italy
Julien Signoles, CEA LIST, France
Tarmo Uustalu, Tallin University of Technology, Estonia
------------------------------
Message-ID: <8C234E92-C23D-418C-B3B0-4ABE3352BBA9 at ifi.uio.no>
Date: Tue, 27 Jun 2017 09:49:54 +0000
From: Ingrid Chieh Yu <ingridcy at ifi.uio.no>
Subject: [FME Events] [iFM'17] Call for Participation for the International
Conference on integrated Formal Methods 2017
********************************************************************************
iFM 2017 - CALL FOR PARTICIPATION
13th International Conference on integrated Formal Methods
18-22 September 2017, Turin, Italy
http://ifm2017.di.unito.it/
********************************************************************************
We warmly invite you to take part in the 13th International Conference on
integrated Formal Methods, which will take place at Turin University between
Monday 18 and Friday 22 September, 2017.
Applying formal methods may involve the usage of different formalisms and
different analysis techniques to validate a system, either because individual
components are most amenable to one formalism or technique, because one is
interested in different properties of the system, or simply to cope with the
sheer complexity of the system. The iFM conference series seeks to further
research into hybrid approaches to formal modeling and analysis; i.e.,
the combination of (formal and semi-formal) methods for system development,
regarding both modeling and analysis. The conference covers all aspects from
language design through verification and analysis techniques to tools and
their
integration into software engineering practice.
VENUE
=====
University of Turin, Italy
REGISTRATION
============
* Registration is now open at http:
http://ifm2017.di.unito.it/registration.php
* Early registration deadline: Monday, July 24, 2017
RESEARCH PROGRAM
================
Preliminary program is available at http://ifm2017.di.unito.it/program.php
INVITED SPEAKERS
================
* Jane Hillston (University of Edinburgh, UK)
* André Platzer (Carnegie Mellon University, USA)
* Matrin Vechev (ETH Zurich, Switzerland)
DOCTORAL SYMPOSIUM
==================
The doctoral symposium offers an excellent opportunity to PhD students and
young
researchers to present their work in an international setting, and to get
feedback from senior researchers in the field.
CO-LOCATED WORKSHOPS
====================
* FMICS-AVoCS: International Workshop on Formal Methods for Industrial
Critical
Systems (FMICS) and Automated Verification of Critical Systems (AVoCS)
* ALP4IoT: Architectures, Languages and Paradigms for IoT
* WAO: Actors and Active Objects
* FVAV: Formal Verification of Autonomous Vehicles
* PrePost: Pre- and post-deployment verification techniques
* V2CPS: Verification and Validation of Cyber-Physical Systems
UPDATES
=======
For up-to-date information, please check iFM's website and Twitter:
Website: http://ifm2017.di.unito.it/
Twitter: https://twitter.com/iFMconf, @iFMconf
—
Ingrid Chieh Yu
Associate professor
Dept. of Informatics, University of Oslo
Tel + 47 2284 5525, email ingridcy at ifi.uio.no<mailto:ingridcy at ifi.uio.no>
------------------------------
*********************************************
End of it-fmeurope-events Digest Tue, 04 Jul 2017
More information about the ecoop-info
mailing list