From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id E93897FA4D for ; Tue, 29 Jul 2014 06:16:41 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of fm-announcements-bounces@lists.nasa.gov) identity=pra; client-ip=128.156.249.229; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="fm-announcements-bounces@lists.nasa.gov"; x-sender="fm-announcements-bounces@lists.nasa.gov"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of fm-announcements-bounces@lists.nasa.gov designates 128.156.249.229 as permitted sender) identity=mailfrom; client-ip=128.156.249.229; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="fm-announcements-bounces@lists.nasa.gov"; x-sender="fm-announcements-bounces@lists.nasa.gov"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of postmaster@lists.nasa.gov designates 128.156.249.229 as permitted sender) identity=helo; client-ip=128.156.249.229; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="fm-announcements-bounces@lists.nasa.gov"; x-sender="postmaster@lists.nasa.gov"; x-conformance=sidf_compatible; x-record-type="v=spf1" X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AngCAKYf11OAnPnlm2dsb2JhbABZgkeBGVcBgnfHMoFYAQmIYRYQAQEBAQEICQsJFCmEBQYBARoGIwgCFgIFAQ4DAQIGAgg6AgQEAgIDASQJLBMFGASIIQ2LBJwwl1YXjB0BgkwRAQuDBA8yEiSBGwWKcY1qhEOFNBiETIxLTAGBBAcXBg X-IPAS-Result: AngCAKYf11OAnPnlm2dsb2JhbABZgkeBGVcBgnfHMoFYAQmIYRYQAQEBAQEICQsJFCmEBQYBARoGIwgCFgIFAQ4DAQIGAgg6AgQEAgIDASQJLBMFGASIIQ2LBJwwl1YXjB0BgkwRAQuDBA8yEiSBGwWKcY1qhEOFNBiETIxLTAGBBAcXBg X-IronPort-AV: E=Sophos;i="5.01,754,1400018400"; d="scan'208,217";a="87354116" Received: from lists.nasa.gov ([128.156.249.229]) by mail2-smtp-roc.national.inria.fr with ESMTP; 29 Jul 2014 06:16:38 +0200 Received: from localhost (localhost [127.0.0.1]) by lists.nasa.gov (Postfix) with ESMTP id 7DCEE6012B7; Tue, 29 Jul 2014 00:15:27 -0400 (EDT) Received: from lists.nasa.gov ([127.0.0.1]) by localhost (lists.nasa.gov [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id rc45c6qxoBf7; Tue, 29 Jul 2014 00:15:27 -0400 (EDT) Received: from lists.nasa.gov (localhost [127.0.0.1]) by lists.nasa.gov (Postfix) with ESMTP id 88CD660103B; Tue, 29 Jul 2014 00:15:24 -0400 (EDT) X-Original-To: fm-announcements@lists.nasa.gov Delivered-To: fm-announcements@lists.nasa.gov Received: from localhost (localhost [127.0.0.1]) by lists.nasa.gov (Postfix) with ESMTP id B84FF6000B2 for ; Tue, 29 Jul 2014 00:15:21 -0400 (EDT) Received: from lists.nasa.gov ([127.0.0.1]) by localhost (lists.nasa.gov [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id fCdgwuBm9mA2 for ; Tue, 29 Jul 2014 00:15:21 -0400 (EDT) Received: from mail.jpl.nasa.gov (mailhost.jpl.nasa.gov [128.149.139.106]) by lists.nasa.gov (Postfix) with ESMTP id 549AF60002C for ; Tue, 29 Jul 2014 00:15:18 -0400 (EDT) Received: from [192.168.0.7] (cpe-76-171-10-135.socal.res.rr.com [76.171.10.135]) (authenticated (0 bits)) by smtp.jpl.nasa.gov (Sentrion-MTA-4.3.1/Sentrion-MTA-4.3.1) with ESMTP id s6T4FGqt019569 (using TLSv1/SSLv3 with cipher AES128-SHA (128 bits) verified NO) for ; Mon, 28 Jul 2014 21:15:17 -0700 From: Klaus Havelund Message-Id: <541139D4-6213-40F6-86D1-E9A259806E9A@jpl.nasa.gov> Date: Mon, 28 Jul 2014 21:15:16 -0700 To: "fm-announcements@lists.nasa.gov" Mime-Version: 1.0 (Mac OS X Mail 6.6 \(1510\)) X-Mailer: Apple Mail (2.1510) X-Source-Sender: klaus.havelund@jpl.nasa.gov X-JPL-Spam-Score': 80% X-BeenThere: fm-announcements@lists.nasa.gov X-Mailman-Version: 2.1.14 List-Id: NASA Formal Methods Announcements List-Unsubscribe: , List-Post: List-Help: List-Subscribe: , Content-Type: multipart/mixed; boundary="===============0758502183863622618==" Errors-To: fm-announcements-bounces@lists.nasa.gov Sender: fm-announcements-bounces@lists.nasa.gov X-Validation-by: klaus.havelund@jpl.nasa.gov Subject: [Caml-list] [fm-announcements] RV 2014: Call for Participation --===============0758502183863622618== Content-Type: multipart/alternative; boundary="Apple-Mail=_784FDB7B-9DB4-4550-B040-AA361285D429" --Apple-Mail=_784FDB7B-9DB4-4550-B040-AA361285D429 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 CALL FOR PARTICIPATION RV 2014: 14th International Conference on Runtime Verification September 22 - September 25, 2014, Toronto, Canada http://rv2014.imag.fr OVERVIEW Runtime verification is concerned with monitoring and analysis of software = and hardware system executions. Runtime verification techniques are importa= nt for system correctness, reliability, and robustness; they are complement= ary to conventional testing, and more practical than exhaustive formal veri= fication. Runtime verification can be used prior to deployment, for testing= , verification, and debugging purposes, and after deployment for ensuring r= eliability, safety, and security and for providing fault containment and re= covery as well as online system repair. Topics of interest to the conferenc= e include: specification languages specification mining program instrumentation monitor construction techniques logging, recording, and replay fault detection, localization, containment, recovery and repair program steering and adaptation metrics and statistical information gathering combination of static and dynamic analyses program execution visualization monitoring techniques for safety/mission-critical systems monitoring distributed systems, cloud services, and big data applications monitoring security and privacy policies Application areas of runtime verification include safety/mission-critical s= ystems, enterprise and systems software, autonomous and reactive control sy= stems, health management and diagnosis systems, and system security and pri= vacy. INVITED TALKS Kevin Driscoll Fellow at Honeywell Labs, USA Murphy Strikes Again Assaf Schuster Professor of Computer Science, Computer Science Department, Technion, Israel Monitoring Big, Distributed, Streaming Data Jeannette Wing President's Professor of Computer Science, Computer Science Department, Carnegie Mellon University, USA Formal Methods: An Industrial Perspective INVITED TUTORIALS Vijay K. Garg & Neeraj Mittal UT at Austin & UT at Dallas A Lattice-Theoretic Approach to Monitoring Distributed Computations David Basin & Felix Klaedtke ETH-Zurich & NEC Labs, Europe Runtime Monitoring and Enforcement of Security Policies VENUE The Fields Institute for Research in Mathematical Sciences 222 College Street, Toronto, Ontario, Canada http://www.fields.utoronto.ca/ REGISTRATION Registration on line to Aug. 21, on site Sept. 22 Registration fees $575, after Aug. 21 $675 Student $350, after Aug. 21, $450 Fees include proceedings and 1x Conference banquet Additional banquet tickets $80 Registration link: http://www.fields.utoronto.ca/programs/scientific/14-15/RV2014/ ACCEPTED PAPERS Pierre Fraigniaud, Sergio Rajsbaum and Corentin Travers.=20 On the Number of Opinions Needed for Fault-Tolerant Run-Time Monitoring in = Distributed Systems Simon Varvaressos, Kim Lavoie, Sebastien Gaboury and Sylvain Hall=C3=A9. Multiple Ways to Fail: Generalizing a Monitor's Verdict for the Classificat= ion of Execution Traces Clemens Ballarin. Two Generalisations of Ro=C5=9Fu and Chen's Trace Slicing Algorithm A Martin Hentschel, Richard Bubel and Reiner H=C3=A4hnle. Symbolic Execution Debugger (SED)=20 Jiannan Zhai, Nigamanth Sridhar and Jason Hallstrom. Supporting the Specification and Runtime Validation of Asynchronous Calling= Patterns in Reactive Systems=20 Emmanouil Koukoutos and Viktor Kuncak. Checking Data Structure Properties Orders of Magnitude Faster=20 Maria Christakis, Patrick Emmisberger and Peter M=C3=BCller. Dynamic Test Generation with Static Fields and Initializers=20 Aravind Sukumaran-Rajam, Juan Manuel Martinez Caamano, Willy Wolff, Alexand= ra Jimborean and Philippe Clauss. Speculative Program Parallelization with Scalable and Decentralized Runtime= Verification=20 Christian Colombo and Yli=C3=A8s Falcone. Organising LTL Monitors over Distributed Systems with a Global Clock=20 Erdal Mutlu, Vladimir Gajinov, Adrian Cristal, Serdar Tasiran and Osman Uns= al. Dynamic Verification for Hybrid Concurrent Programming Models=20 Hsi-Ming Ho, Joel Ouaknine and James Worrell. Online Monitoring of Metric Temporal Logic David Basin, Germano Caronni, Sarah Ereth, Mat=C3=BA=C5=A1 Harvan, Felix Kl= aedtke and Heiko Mantel. Scalable Offline Monitoring=20 David Basin, Felix Klaedtke, Srdjan Marinovic and Eugen Zalinescu. On Real-time Monitoring with Imprecise Timestamps=20 Anand Yeolekar. Improving dynamic inference with variable dependence graph=20 Ming Chai and Holger Schlingloff. Monitoring Systems with Extended Live Sequence Charts=20 Laura Bozzelli and C=C3=A9sar S=C3=A1nchez. Foundations of Boolean Stream Runtime Verification=20 Mitra Tabaei Befrouei, Chao Wang and Georg Weissenbacher. Abstraction and Mining of Traces to Explain Concurrency-Bugs=20 Stefan Mitsch and Andr=C3=A9 Platzer. ModelPlex: Verified Runtime Validation of Verified Cyber-Physical System Mo= dels=20 Johannes Geist, Kristin Y. Rozier and Johann Schumann. Runtime Observer Pairs and Bayesian Network Reasoners On-board FPGAs: Fligh= t-Certifiable System Health Management for Embedded Systems=20 Malte Isberner, Falk Howar and Bernhard Steffen The TTT Algorithm: A Redundancy-Free Approach to Active Automata Learning Kim Lavoie, Corentin Leplongeon, Simon Varvaressos, Sebastien Gaboury and S= ylvain Hall=C3=A9. Portable Runtime Verification with Smartphones and Optical Codes=20 Adel Dokhanchi, Bardh Hoxha and Georgios Fainekos On-Line Monitoring for Temporal Logic Robustness=20 Jeff Huang, Cansu Erdogan, Yi Zhang, Brandon Moore, Qingzhou Luo, Aravind S= undaresan and Grigore Rosu. ROSRV: Runtime Verification for Robots=20 Qingzhou Luo, Yi Zhang, Choonghwan Lee, Dongyun Jin, Patrick Meredith, Trai= an Serbanuta and Grigore Rosu. RV-Monitor: Efficient Parametric Runtime Verification with Simultaneous Pro= perties=20 Duc Hiep Chu, Joxan Jaffar and Vijayaraghavan Murali. Lazy Symbolic Execution for Enhanced Learning=20 Kuei Sun, Daniel Fryer, Ashvin Goel, Dai Qin and Angela Demke Brown. Robust Consistency Checking for Modern Filesystems=20 Ayoub Nouri, Balaji Raman, Marius Bozga, Axel Legay and Saddek Bensalem. Faster Statistical Model Checking by Means of Abstraction and Learning CHAIRS AND ORGANIZERS General Chair: Sebastian Fischmeister (University of Waterloo, Canada). PC co-Chairs:=20 Borzoo Bonakdarpour (McMaster University, Canada) Scott Smolka (Stony Brook Universtiy, USA) Tools Track Chair: Ezio Bartocci (TU Vienna, Austria) Runtime Monitoring Competition Co-Chairs: Ezio Bartocci (TU Vienna, Austria) Borzoo Bonakdarpour (McMaster University, Canada) Ylies Falcone (Universit=C3=A9 Joseph Fourier, France) Publicity Chair: Ylies Falcone (Universit=C3=A9 Joseph Fourier, France) Local Arrangements Chair: Patrick Lam (University of Waterloo, Canada) FURTHER INFORMATION More information about RV2014 is available from the conference web site: http://rv2014.imag.fr= --Apple-Mail=_784FDB7B-9DB4-4550-B040-AA361285D429 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=utf-8

CALL FOR PARTICIPATION

RV 2014: 14th International Conf= erence on Runtime Verification

Sept= ember 22 - September 25, 2014, Toronto, Canada

http://rv2014.imag.fr<= /a>


OVERVIEW

Runtime ver= ification is concerned with monitoring and analysis of software and hardwar= e system executions. Runtime verification techniques are important for syst= em correctness, reliability, and robustness; they are complementary to conv= entional testing, and more practical than exhaustive formal verification. R= untime verification can be used prior to deployment, for testing, verificat= ion, and debugging purposes, and after deployment for ensuring reliability,= safety, and security and for providing fault containment and recovery as w= ell as online system repair. Topics of interest to the conference include:<= /p>

Application areas of runtime verificat= ion include safety/mission-critical systems, enterprise and systems softwar= e, autonomous and reactive control systems, health management and diagnosis= systems, and system security and privacy.


INVIT= ED TALKS



INVITED TUTORIALS



VENUE


The Fields Institute for Research= in Mathematical Sciences

222 College Street, Toronto, Ontario, Canada

http://www.fields.utoronto= .ca/


Registration on line to Aug. 21, on site Sept. 22

Registration fees $575, after&nbs= p;Aug. 21 $675

S= tudent $350, after Aug. 21, $450


= Fees include proceedings and 1x Conference banquet

Additional banquet tickets $80


Registration link:

ht= tp://www.fields.utoronto.ca/programs/scientific/14-15/RV2014/=


ACCEPTED PAPERS


  • Pierre Fraigniaud, Sergio Rajsbaum and Corentin Travers. On the Number of Opinions Needed for Fault-Tolerant Run-Time Monitoring i= n Distributed Systems
  • Simon Varvaress= os, Kim Lavoie, Sebastien Gaboury and Sylvain Hall=C3=A9.
    Multiple Ways = to Fail: Generalizing a Monitor's Verdict for the Classification of Executi= on Traces
  • Clemens Ballarin.
    Two Ge= neralisations of Ro=C5=9Fu and Chen's Trace Slicing Algorithm A
  • Martin Hentschel, Richard Bubel and Reiner H=C3= =A4hnle.
    Symbolic Execution Debugger (SED) 
  • Jiannan Zhai, Nigamanth Sridhar and Jason Hallstrom.
    Supp= orting the Specification and Runtime Validation of Asynchronous Calling Pat= terns in Reactive Systems 
  • Emman= ouil Koukoutos and Viktor Kuncak.
    Checking Data Structure Properties Ord= ers of Magnitude Faster 
  • Maria C= hristakis, Patrick Emmisberger and Peter M=C3=BCller.
    Dynamic Test Gener= ation with Static Fields and Initializers 
  • Aravind Sukumaran-Rajam, Juan Manuel Martinez Caamano, Willy Wol= ff, Alexandra Jimborean and Philippe Clauss.
    Speculative Program Paralle= lization with Scalable and Decentralized Runtime Verification 
    • Christian Colombo and Yli=C3=A8s Falcone.Organising LTL Monitors over Distributed Systems with a Global Clock =
  • Erdal Mutlu, Vladimir Gajinov, Adria= n Cristal, Serdar Tasiran and Osman Unsal.
    Dynamic Verification for Hybr= id Concurrent Programming Models 
  • David Basin, Germa= no Caronni, Sarah Ereth, Mat=C3=BA=C5=A1 Harvan, Felix Klaedtke and Heiko M= antel.
    Scalable Offline Monitoring 
  • David Basin, Felix Klaedtke, Srdjan Marinovic and Eugen Zalinescu.On Real-time Monitoring with Imprecise Timestamps 
  • Anand Yeolekar.
    Improving dynamic inference with va= riable dependence graph 
  • Ming Ch= ai and Holger Schlingloff.
    Monitoring Systems with Extended Live Sequenc= e Charts 
  • Laura Bozzelli and C= =C3=A9sar S=C3=A1nchez.
    Foundations of Boolean Stream Runtime Verificati= on 
  • Mitra Tabaei Befrouei, Chao = Wang and Georg Weissenbacher.
    Abstraction and Mining of Traces to Explai= n Concurrency-Bugs 
  • Stefan Mitsc= h and Andr=C3=A9 Platzer.
    ModelPlex: Verified Runtime Validation of Veri= fied Cyber-Physical System Models 
  • Malte Isberner, Falk Howar and Bernhard Steffen
    The TTT A= lgorithm: A Redundancy-Free Approach to Active Automata Learning
  • Kim Lavoie, Corentin Leplongeon, Simon Varvares= sos, Sebastien Gaboury and Sylvain Hall=C3=A9.
    Portable Runtime Verifica= tion with Smartphones and Optical Codes 
  • Adel Dokhanchi, Bardh Hoxha and Georgios Fainekos
    On-Line Monit= oring for Temporal Logic Robustness 
  • Jeff Huang, Cansu Erdogan, Yi Zhang, Brandon Moore, Qingzhou Luo, Arav= ind Sundaresan and Grigore Rosu.
    ROSRV: Runtime Verification for Robots&= nbsp;
  • Qingzhou Luo, Yi Zhang, Choongh= wan Lee, Dongyun Jin, Patrick Meredith, Traian Serbanuta and Grigore Rosu.<= br>RV-Monitor: Efficient Parametric Runtime Verification with Simultaneous = Properties 
  • Duc Hiep Chu, Joxan = Jaffar and Vijayaraghavan Murali.
    Lazy Symbolic Execution for Enhanced L= earning 
  • Kuei Sun, Daniel Fryer,= Ashvin Goel, Dai Qin and Angela Demke Brown.
    Robust Consistency Checkin= g for Modern Filesystems 
  • Ayoub = Nouri, Balaji Raman, Marius Bozga, Axel Legay and Saddek Bensalem.
    Faste= r Statistical Model Checking by Means of Abstraction and Learning
=


CHAIRS AND ORGANIZERS


  • General Chair: Sebastian= Fischmeister (University of Waterloo, Canada).
  • PC co-Chairs: 
    • Bo= rzoo Bonakdarpour (McMaster University, Canada)
    • Scott Smolka (Stony Brook Universtiy, USA)
  • Tools Track Chair: Ezio Bartocci (TU Vienna, Austria)=
  • Runtime Monitoring Competition Co-Ch= airs:
    • Ezio Bartocci (TU Vienna, A= ustria)
    • Borzoo Bonakdarpour (McMaster= University, Canada)
    • Ylies Falcone (U= niversit=C3=A9 Joseph Fourier, France)
  • Publicity Chair: Ylies Falcone (Universit=C3=A9 Joseph Fourier, Fran= ce)
  • Local Arrangements Chair: Patrick= Lam (University of Waterloo, Canada)


FURTHER INFORMATION


More information about RV2014 is available from the confe= rence web site:

http://rv2014.imag.fr

= --Apple-Mail=_784FDB7B-9DB4-4550-B040-AA361285D429-- --===============0758502183863622618== Content-Type: text/plain; charset="us-ascii" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit Content-Disposition: inline --- To opt-out from this mailing list, send an email to fm-announcements-request@lists.nasa.gov with the word 'unsubscribe' as subject or in the body. You can also make the request by contacting fm-announcements-owner@lists.nasa.gov --===============0758502183863622618==--