Workshop on Formal Approaches to Explainable VERification (FEVER 2017)

JULY 23, 2017, HEIDELBERG, GERMANY

Co-Located with CAV 2017

This workshop will focus on the problem of rendering the results of formal verification more understandable to humans, and on the inherent problem of requiring explanations for the results of formal verification. As we are also interested in formal measures to explainability, this is the problem of 'Formal approaches to Explainable VERification’ (FEVER).

Traditionally, formal verification aims to provide guarantees on the behavior of a system model. We believe, however, that the FEVER problem is not sufficiently addressed by state-of-the-art techniques. We see FEVER as a significant new research opportunity for the Computer-Aided Verification community. The traditional modeling and verification processes suffer from their inherent complexity, which makes it hard for non-specialists to understand and rely on them. Formal measures of explainability will contribute to establishing trust in such methods.

The workshop seeks to bring together researchers with diverse expertise, including CAV, AI, VR (Virtual Reality), and HCI (Human-Computer Interaction), to lay down the foundations for this new topic and to discuss existing approaches, ideas, and challenges.

Topics include, but are not limited to:

  • understandable modeling languages, such as probabilistic programs
  • accessible synthesis results and abstraction techniques
  • explainable counterexamples and controllers
As there are no formal proceedings for the workshop, the main focus is on a broad range of topics that trigger lively discussions.

For any kind of questions please contact Nils Jansen at n.jansen@science.ru.nl

News

July 3, 2017The program is online.
June 7, 2017The accepted contributions are online. We have an excellent program!
Apr 7, 2017Call for contributions, important dates, and invited speakers have been added.
Jan 25, 2017Website is online.

Program

8:45 - 9:00Welcome
9:00 - 10:00Invited Talk Holger Hermanns, Saarland University, Germany

What Diesel Engines teach us about Embedded Software Verification
10:00 - 10:25Thomas Ferrère, Oded Maler and Dejan Nickovic: Trace Diagnostics using Temporal Implicants
10:30 - 11:00Coffee Break
11:00 - 12:30
  • Viktor Schuppan: A Framework for Comparing the Granularity of Unsatisfiable Cores, Vacuity, and Related Notions
  • Taylor T Johnson: Reusable and Understandable Formal Verification for Cyber-Physical Systems
  • Arnd Hartmanns: JANI for Modelling and Tool Interaction
  • Murat Cubuktepe, Nils Jansen and Ufuk Topcu: Inverse Reinforcement Learning to Capture Human Intent in a Shared Control Setting
12:30 - 14:00Lunch
14:00 - 15:00Invited Talk Roderick Bloem, TU Graz, Austria

Shields - Runtime Enforcement for Reactive Systems
15:00 - 15:25Tomas Brazdil, Krishnendu Chatterjee, Jan Kretinsky and Viktor Toman: Strategy Representation by Decision Trees
15:30 - 16:00Coffee Break
16:00 - 17:00
  • Hillel Kugler: Explainable Verification-Based Approaches in Systems Biology
  • Rayna Dimitrova, Rupak Majumdar and Vinayak Prabhu: Causality Analysis for Concurrent Reactive Systems
  • Takamasa Okudono, Yuki Nishida, Kensuke Kojima, Kohei Suenaga, Kengo Kido and Ichiro Hasuo: Sharper and Simpler Nonlinear Interpolants for Program Verification

Invited Speakers

  • Roderick Bloem, TU Graz, Austria

    Shields - Runtime Enforcement for Reactive Systems

    It is difficult to write correct systems, it is difficult to verify that systems are correct, and it is even difficult to specify what exactly a good system should do. Ideally, a designer should only be required to specify crucial properties, and these properties should be enforced even if the system cannot be verified. We will discuss shields a runtime enforcement methods for reactive systems, and its application to learned systems, which almost always work very well, but cannot be shown to always work acceptably.

  • Holger Hermanns, Saarland University, Germany

    What Diesel Engines teach us about Embedded Software Verification

Accepted Contributions

  • Thomas Ferrère, Oded Maler and Dejan Nickovic: Trace Diagnostics using Temporal Implicants
  • Viktor Schuppan: A Framework for Comparing the Granularity of Unsatisfiable Cores, Vacuity, and Related Notions
  • Taylor T Johnson: Reusable and Understandable Formal Verification for Cyber-Physical Systems
  • Arnd Hartmanns: JANI for Modelling and Tool Interaction
  • Murat Cubuktepe, Nils Jansen and Ufuk Topcu: Inverse Reinforcement Learning to Capture Human Intent in a Shared Control Setting
  • Tomas Brazdil, Krishnendu Chatterjee, Jan Kretinsky and Viktor Toman: Strategy Representation by Decision Trees
  • Hillel Kugler: Explainable Verification-Based Approaches in Systems Biology
  • Rayna Dimitrova, Rupak Majumdar and Vinayak Prabhu: Causality Analysis for Concurrent Reactive Systems
  • Takamasa Okudono, Yuki Nishida, Kensuke Kojima, Kohei Suenaga, Kengo Kido and Ichiro Hasuo: Sharper and Simpler Nonlinear Interpolants for Program Verification

Program Committee

Call for Contributions

The FEVER workshop solicits presentations of ongoing or previously published work to enable discussions on a broad range of topics. These presentations will not be subject to proceedings publication. We encourage all interested authors to submit an abstract of their presentation through Easychair:

https://easychair.org/conferences/?conf=fever2017

We particularly invite work recently accepted to top conferences and ongoing work. The submission should be a pdf of at most two pages in the llncs style.

Important Dates:

  • Abstract submission: May 28, 2017 (new)
  • Notification: May 30, 2017
  • Workshop: July 23, 2017