[ecoop-info] it-fmeurope-events Digest Tue, 25 Jul 2017

it-fmeurope-events-request at lists.uu.se it-fmeurope-events-request at lists.uu.se
Tue Jul 25 10:00:14 CEST 2017

it-fmeurope-events digest Tue, 25 Jul 2017

Table of contents:

* 1 - [FME Events] RV 2017 - 1st Call for Participation - Ayoub Nouri
  <ayoub.nouri at univ-grenoble-alpes.fr>
* 2 - [FME Events] Second CFP IMPEX2017 : First International Workshop on
  Handling IMPlicit and EXplicit knowledge in formal system development. -
  mery <dominique.mery at loria.fr>
* 3 - [FME Events] SEFM 2017 -- Call for Participation - Alberto Griggio
  <griggio at fbk.eu>
* 4 - [FME Events] HVC 2017 - Submission Deadline Extended - "Tali Rabetti"
  <TALIS at il.ibm.com>


Message-ID: <0318af5f-6505-2a5a-67af-9df02d92aff5 at univ-grenoble-alpes.fr>
Date: Wed, 19 Jul 2017 17:15:02 +0200
From: Ayoub Nouri <ayoub.nouri at univ-grenoble-alpes.fr>
Subject: [FME Events] RV 2017 - 1st Call for Participation



The 17th International Conference on Runtime Verification, September
13-16 2017, Seattle, WA, USA


Affiliated Event:

RV-CuBES - An International Workshop on Competitions, Usability,
Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools

=== OVERVIEW ===

Runtime verification is concerned with the monitoring and analysis of
the runtime behaviour of software and hardware systems. Runtime
verification techniques are crucial for system correctness, reliability,
and robustness; they provide an additional level of rigor and
effectiveness compared to conventional testing, and are generally more
practical than exhaustive formal verification. Runtime verification can
be used prior to deployment, for testing, verification, and debugging
purposes, and after deployment for ensuring reliability, safety, and
security and for providing fault containment and recovery as well as
online system repair. Topics of interest to the conference include:

    specification languages

    monitor construction techniques

    program instrumentation

    logging, recording, and replay

    combination of static and dynamic analysis

    specification mining and machine learning over runtime traces

    monitoring techniques for concurrent and distributed systems

    runtime checking of privacy and security policies

    statistical model checking

    metrics and statistical information gathering

    program/system execution visualization

    fault localization, containment, recovery and repair

    integrated vehicle health management (IVHM)

Application areas of runtime verification include cyber-physical
systems, safety/mission-critical systems, enterprise and systems
software, autonomous and reactive control systems, health management and
diagnosis systems, and system security and privacy.


Rodrigo Fonseca, Brown University, USA:

          “The Design and Applications for a Tracing Plane for
Distributed Systems”

Vlad Levin and Jakob Lichtenberg, Microsoft, USA:

          “Windows Driver Verification Platform”

Andreas Zeller, Saarland University, Germany:

          “Learning Input Languages for Runtime Verification”


Ankush Desai and Shaz Qadeer, UC Berkeley and Microsoft Research, USA:

          “P : Modular and Safe Asynchronous Programming”

Madhusudan Parthasarathy, University of Illinois at Urbana-Champaign, USA:

          “Machine-learning State Properties”

Adrian Francalanza, University of Malta, Malta:

          “Foundations For Runtime Monitoring”


=== Regular Papers

Bernhard K. Aichernig and Martin Tappler.

“Probabilistic Black-Box Reachability Checking”

Minjun Seo and Roman Lysecky.

“Hierarchical Non-Intrusive In-Situ Requirements Monitoring for Embedded

David Basin, Srđan Krstić and Dmitriy Traytel.

“Almost Event-Rate Independent Monitoring of Metric Dynamic Logic”

Kostyantyn Vorobyov, Nikolai Kosmatov, Julien Signoles and Arvid Jakobsson.

“Runtime Detection of Temporal Memory Errors”

Katarína Kejstová, Petr Ročkai and Jiri Barnat.

“From Model Checking to Runtime Verification and Back”

Zachary Benavides, Rajiv Gupta and Xiangyu Zhang.

“Annotation Guided Collection of Context-Sensitive Parallel Execution

Oliviero Riganelli, Daniela Micucci, Leonardo Mariani and Yliès Falcone.

“Verifying Policy Enforcers”

Ankush Desai, Tommaso Dreossi and Sanjit A. Seshia.

“Combining Model Checking and Runtime Verification for Safe Robotics”

Vidhya Tekken Valapil, Sorrachai Yingchareonthawornchai, Sandeep
Kulkarni, Eric Torng and Murat Demirbas.

“Monitoring Partially Synchronous Distributed Systems using SMT Solvers”

Chaoqiang Deng and Kedar Namjoshi.

“Witnessing Network Transformations”

Teng Zhang, John Wiegley, Insup Lee and Oleg Sokolsky.

“Monitoring Time Intervals”

Bjorn Andersson, Sagar Chaki and Dionisio De Niz.

“Combining Symbolic Runtime Enforcers for Cyber-Physical Systems”

Babak Yadegari and Saumya Debray.

“Control Dependencies in Interpretive Systems”

Himanshu Chauhan and Vijay Garg.

“Space Efficient Breadth-First and Level Traversals of Consistent Global
States of Parallel Programs”

Giuseppe Bombara and Calin Belta.

“Signal Clustering using Temporal Logics”

Susmit Jha, Ashish Tiwari, Sanjit A. Seshia, Natarajan Shankar and Tuhin

“TeLEx: Passive STL Learning Using Only Positive Examples”

Florian-Michael Adolf, Peter Faymonville, Bernd Finkbeiner, Sebastian
Schirmer and Christoph Torens. “Stream Runtime Monitoring on UAVs”

Bernd Finkbeiner, Christopher Hahn, Marvin Stenger and Leander Tentrup.

“Monitoring Hyperproperties”

=== Tool Papers

Hassan Salehe Matar and Serdar Tasiran.

“EmbedSanitizer: Runtime Race Detection Tool for 32-bit Embedded ARM”

Prashanth Nayak, Mike Hibler, David Johnson and Eric Eide.

“A Wingman for Virtual Appliances”

Shuo Chen.

“SVAuth – A Single-Sign-On Integration Solution with Runtime Verification”

Raphael Khoury, Sebastien Gaboury and Sylvain Hallé.

“Event Stream Processing with Multiple Threads”

Daisuke Ishii and Alexandre Goldsztejn.

“HySIA: Tool for Simulating and Monitoring Hybrid Automata Based on
Interval Analysis”

=== Short Papers

Kim Völlinger.

“Verifying the Output of a Distributed Algorithm using Certification”

Chafik Meniar, Florence Opalvens and Sylvain Hallé.

“Runtime Verification of User Interface Guidelines in Mobile Devices”

Aaron Paulos, Partha Pal, Shane Clark, Kyle Usbeck and Patrick Hurley.

“Trusted Mission Operation – Concept and Implementation”

Jun Inoue and Yoriyuki Yamagata.

“Operational Semantics of Process Monitors”

=== VENUE ===

The 17th International Conference on Runtime Verification will be held
in the Sheraton Seattle Hotelsituated in downtown Seattle. The venue is
within walking distance of the famous Pike Place Market, Seattle Art
Museum, Seattle Aquarium, and the Historic Seattle Waterfront. The
weather in September still permits many open-air opportunities to shop,
eat, and even sail in the Elliott Bay. Exceptionally well organized,
Seattle’s public transport connects the conference venue with the
Seattle Center, which is the home of popular attractions like the Space
Needle, EMP Museum, and Chihuly Garden and Glass.


Registration is now available using the web-based registration form,
with online payment on a secure website. Please use one form per
attendee. Early registration means on or before August 13, 2017. Late
registration means after August 13, 2017.

Different possibilities of registration are available:

     Tutorial Day Only (13th September): 210 USD

     Conference including tutorial day and RV-CuBES (13-16th September)

            Full Registration

                Early: 680 USD,

                Late (after 13 August): 780 USD

            Student Registration

                Early: 480 USD,

                Late (after 13 August): 580 USD


General Chair

    Klaus Havelund, NASA Jet Propulsion Laboratory, USA

Program Chairs

    Shuvendu Lahiri, Microsoft Research, USA

    Giles Reger, University of Manchester, UK

Finance Chair

    Oleg Sokolsky, University of Pennsylvania, USA

Publicity Chair

    Ayoub Nouri, University of Grenoble Alpes, France

Local Organisation Chairs

    Grigory Fedyukovich, University of Washington, USA

    Rahul Kumar, Microsoft Research, USA

RV-CuBES, PC chairs

    Giles Reger, University of Manchester, UK

    Klaus Havelund, NASA Jet Propulsion Laboratory, USA

=== SPONSORS ===



--- end --

Message-ID: <62cc6f56-1c5f-0db7-379c-37cc66534f93 at loria.fr>
Date: Mon, 17 Jul 2017 23:07:08 +0200
From: mery <dominique.mery at loria.fr>
Subject: [FME Events] Second CFP IMPEX2017 : First International Workshop on
 Handling IMPlicit and EXplicit knowledge in formal system development.



    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, Focalize,
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

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://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.


  *      Preliminary proceedings, including all the papers selected for
    the workshop, will be available electronically at the workshop.

  *      Post proceedings will be published  after the workshiop with
    Electronic Proceedings in Theoretical Computer Science (EPTCS).

*Important Dates**

  * Abstract Submission: 26 August 2017

  * Full Paper Submission: 2 September 2017

  * Acceptance/Rejection Notification: 1 October  2017

  *   Camera-ready Paper for preliminary proceedings: October 28, 2017

  *    Camera-ready Paper for post-proceedings: 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,

     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

     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,

     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


Papers accepted for presentation will  be published in EPTCS. 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

Message-ID: <20170720151408.6E9C615F9F4 at kyrene.fbk.eu>
Date: Thu, 20 Jul 2017 17:14:08 +0200
From: Alberto Griggio <griggio at fbk.eu>
Subject: [FME Events] SEFM 2017 -- Call for Participation


                      SEFM 2017 - Call for Participation

                        15th International Conference
                  on Software Engineering and Formal Methods

                      September 4-8, 2017, Trento, Italy




- Marsha Chechik (University of Toronto, Canada)
- Jeff Kramer (Imperial College London, United Kingdom)
- Alberto Sangiovanni-Vincentelli (Berkeley University, United States)


- FAACS. Formal Approaches for Advanced Computing Systems. (4 September)

- MSE. Microservices: Science and Engineering. (4 September)

- POTENTIAL. Workshop on Technology Transfer in Software Engineering and
  Formal Methods (4 September)

- DataMod. From Data to Models and Back. (4-5 September)

- CoSim-CPS. Formal Co-Simulation of Cyber-Physical Systems. (5 September)

- FOCLASA. Workshop on Foundations Of Coordination Languages and Self-Adaptive
  Systems. (5 September)


- International Conference on Computer Safety, Reliability and Security
  (SAFECOMP 2017)

- International Symposium on Model-Based Safety Assessment (MBSA 2017)


The list of accepted papers is available at:

The program is available at:


The registration for SEFM'17 (together with its affiliated workshops and
tutorials) is now open! Early registration with reduced rates ends on August
See all the details at:


The conference and workshops will take place at the Science and Technology Hub
of Fondazione Bruno Kessler.
More information about the venue at:


Message-ID: <OFAC9A0F65.0A9E4E9F-ONC2258161.00236C41-
 C2258161.002386E7 at notes.na.collabserv.com>
Date: Tue, 18 Jul 2017 06:28:03 +0000
From: "Tali Rabetti" <TALIS at il.ibm.com>
Subject: [FME Events] HVC 2017 - Submission Deadline Extended

We apologize if you receive multiple copies of this CFP.
Please distribute to anyone who may be interested.

Thirteenth Haifa Verification Conference 2017
November 13 - 15, 2017
Tutorials: November 13, 2017
Haifa, Israel - Organized by IBM Research - Haifa
HVC Facebook page
HVC is an annual conference dedicated to advancing the state-of the art
and state-of-the-practice in verification and testing. At the conference,
researchers and practitioners from academia and industry network, share
ideas, and ponder the future directions of testing and verification for
hardware, software, and complex hybrid systems.
The common goal of the conference topics and participants is to ensure the
correct functionality and performance of complex systems. HVC is the only
conference that brings together experts from all verification and testing
sub-fields, thereby encouraging the migration of methods and ideas among
HVC 2017 invites the submission of technical papers reporting original
research and experience results in all sub-fields of testing and
verification applicable to software and hardware. The conference includes
the presentation of peer-reviewed, original technical papers, as well as
lectures by guests from industry and academia.

Special theme this year: verification for security
In addition to the traditional HVC topics (see below), we plan at least
one session dedicated to the research and application of verification
techniques in security. At least one of our invited keynote talks will be
dedicated to this topic.
New this year: tool demos category
In addition to the research and poster sessions, we plan to hold a tool
demos session.
The conference proceedings will be published in Springer?s Lecture Notes
in Computer Science series (LNCS), and distributed in digital format to
registered conference participants.
Keynote Speakers
Prof. Eli Ben-Sasson, Technion
Prof. Dino Distefano, Queen Mary, University of London
Prof. Subhasish Mitra, Stanford University
Kedar Namjoshi, Bell Labs, Nokia
Tutorial Speakers
Dr. Dimitris E. Simos, SBA Research, Austria
Litan Ilany, Intel, Israel
Prof. Arie Gurfinkel, University of Waterloo, Canada

Important dates:
·       Submission deadline (all categories): July 21, 2017 - 11.59 pm GMT
 July 28, 2017 - 11.59 pm GMT
·       Author acceptance notification: September 1, 2017
·       Final manuscripts due: September 15, 2017
·       Conference: November 13 - 15, 2017
·       Tutorials: November 13, 2017
Topics of interest to the conference include, but are not limited to:
·       Simulation-based verification
·       Formal and semi-formal specification, modeling, and verification
·       Functional and non-functional software testing
·       Software and hardware equivalence checking
·       SAT/SMT-based verification algorithms
·       Static analysis
·       Model checking
·       High-level stimuli generation
·       Hardware/software co-verification
·       Cloud quality
·       Validation of data-intensive solutions
·       Validation of machine learning algorithms
·       Triage and debug technologies
·       Post-silicon validation including emulation and acceleration
·       Coverage analysis and test minimization
·       Testing of mobile and cloud applications
·       Software artifacts review and inspection
·       Test planning
·       Empirical studies on hardware and software quality
·       Security verification
·       Machine learning techniques for verification
Detailed instructions for electronic submissions can be found on the HVC
conference web site. For additional information regarding paper
submissions, please contact the HVC program chair Ofer Strichman.
The lovely city of Haifa resides on a mountain overlooking the
Mediterranean Sea, and is home to Jews, Muslims, and Christians. Haifa is
also the world center of the Baha?i faith, and the wondrous Baha?i gardens
are a must-see attraction. The conference will be held at IBM Research -
Haifa, situated at the top of the Carmel mountains.
Student grants:
We anticipate a number of student grants to cover part of the travel
expenses for full-time students who are authors of accepted papers.
Precedence in allocation of these travel grants will be to students who
are also presenting a poster at the conference.
General chair: Rachel Tzoref-Brill (rachelt at il.ibm.com)
Program chair: Ofer Strichman (ofers at ie.technion.ac.il)
Local organization: Revivit Yankovich (revivity at il.ibm.com)
Publicity chair: Tali Rabetti (talis at il.ibm.com)
Tutorial chair: Tom Kolan (tomk at il.ibm.com)
For more information, please refer to HVC2017 web page:
Follow us on Facebook

[An attachment of type application/octet-stream was included here]



End of it-fmeurope-events Digest Tue, 25 Jul 2017

More information about the ecoop-info mailing list