[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
CALL FOR PARTICIPATION
RV’17 - RUNTIME VERIFICATION 2017
The 17th International Conference on Runtime Verification, September
13-16 2017, Seattle, WA, USA
http://rv2017.cs.manchester.ac.uk
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.
=== INVITED TALKS ===
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”
=== TUTORIALS ===
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”
=== ACCEPTED PAPERS ===
=== 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
Systems”
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
Profiles”
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
Sahai.
“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 ===
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
=== CHAIRS AND ORGANIZERS ===
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 ===
Microsoft
Springer
--- 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.
================================================================================================
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, 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
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://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.
*Proceedings*
* 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,
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 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
Sponsors
------------------------------
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
http://sefm17.fbk.eu/
============================================================================
INVITED SPEAKERS
- Marsha Chechik (University of Toronto, Canada)
- Jeff Kramer (Imperial College London, United Kingdom)
- Alberto Sangiovanni-Vincentelli (Berkeley University, United States)
WORKSHOPS
- 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)
RELATED EVENTS
- 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:
http://sefm17.fbk.eu/accepted-papers
The program is available at:
http://sefm17.fbk.eu/programme
============================================================================
The registration for SEFM'17 (together with its affiliated workshops and
tutorials) is now open! Early registration with reduced rates ends on August
7.
See all the details at:
http://sefm17.fbk.eu/registration
============================================================================
The conference and workshops will take place at the Science and Technology Hub
of Fondazione Bruno Kessler.
More information about the venue at:
http://sefm17.fbk.eu/venue
============================================================================
------------------------------
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
https://www.research.ibm.com/haifa/conferences/hvc2017
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
domains.
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
----------------------------------------------------------------
Submissions:
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.
----------------------------------------------------------------
Venue:
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:
http://www.research.ibm.com/haifa/conferences/hvc2017
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