-----Early registration deadline is on June 14, 2017!!-----

Workshop on Formal Approaches to Explainable VERification (FEVER 2017)


Co-Located with CAV 2017

This workshop will focus on the problem of rendering the results of formal verificaton 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 expertises, 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 njansen 'at' utexas 'dot' edu


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.

Invited Speakers

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:


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