DIFTS14

International Workshop on Design and Implementation of Formal Tools and Systems

Lausanne, Switzerland October 20, 2014

co-located with FMCAD and MEMOCODE

Workshop Scope

DIFTS (Design and Implementation of Formal Tools and Systems) workshop emphasizes insightful experiences in formal tools and systems design. The workshop provides an opportunity for discussing engineering aspects and various design decisions required to put formal tools and systems into practical use. In the past, we have invited speakers who have shared their deep insights and discussed the practices followed in the Industry towards adopting formal methods. It provides a forum for sharing challenges and solutions that are original with ground breaking results.

The DIFTS workshop is co-located with FMCAD14 and MEMOCODE14.

Topics of Interest

DIFTS takes a broad view of the formal tools/systems area, and solicits contributions from domains including, but not restricted to, decision procedures, verification, testing, validation, diagnosis, debugging, and synthesis. This workshop encourages and appreciates system development activities, and facilitates transparency in the experimentation. It will also serve as a platform to discuss open problems and future challenges in practicing formal methods. Call for Paper CFP (txt).

  • Abstract Submission: July 28, 2014 August 4, 2014. (closed)
  • Paper Submission: August 4, 2014 August 10, 2014. (closed)
  • Author Notification: September 1, 2014.

Program Chairs

Program Committee

Web Masters

  • Rolf Drechsler, University of Bremen, Germany
  • Title: Coverage at the Formal Specification Level
    Authors: Rolf Drechsler, Julia Seiter, Mathias Soeken

    Abstract
    Speaker bio

  • Wolfgang Kunz, University of Kaiserslautern, Germany
  • Title: The big hurdles for FV tools in industrial practice – can we overcome them insystem-level design flows?
    Wolfgang Kunz Dept. of Electrical and Computer Engineering Technische Universität Kaiserslautern, Germany

    Abstract
    Speaker bio

  • Hans-Joerg Peter, Atrenta, France
  • Title: Efficiently using formal verification techniques to reduce power

    Abstract
The workshop specifically solicits contributions with substantial engineering details that often do not get published but have significant practical impact.

Papers in the following two categories are solicited: (a) system category (10 pages, double column, 11pt), and (b) tool category (8 pages, double column, 11pt).

In the system category, we invite papers that have original ideas accompanied with novel integration techniques, adequate design/implementation details, important design choices made and explored, and good experimental results.

In the tool category, we invite papers that focus primarily on the engineering aspects of some known/popular algorithm, with significant emphasis on the design/implementation details, and various design choices made to advance current state-of-the-art approaches.

The page limit for submissions in the system category is 10 pages in double column format and for submissions in the tool category is 8 pages in double column format.

Submission of papers should be made electronically in PDF format via EasyChair. Submission Page.

Evaluation

To keep maintain uniformity and fairness in the reviewing process, the program committee will evaluate the technical contribution of each submission based on the following guidelines: the paper should provide enough details for others to reproduce the results; and should solve a clearly-stated problem that is significant and has wide interest; and the paper should provide enough motivation for the design choices made. Overall, the paper should also clearly identify what the main contributions of the work are.

Publication

All accepted contributions will be included in informal proceedings. High quality submissions will be considered for a special issue of journals such as FMSD (Formal Methods in System Design) or IEEE TC (Transactions on Computers).

Tayfun Gezgin, Raphael Weber and Markus Oertel, Multi-aspect Virtual Integration approach for Real-Time and Safety Properties

Alberto Griggio and Marco Roveri, Comparing Different Variants of the IC3 Algorithm for Hardware Model Checking

Sebastiaan Joosten, Freek Verbeek and Julien Schmaltz, WickedXmas: Designing and Verifying on-chip Communication Fabrics

Daryl Stewart, David Gilday, Daniel Nevill and Thomas Roberts, Processor Memory System Verification using DOGReL: a language for specifying End-to-End properties

Paolo Camurati, Carmelo Loiacono, Paolo Pasini, Denis Patti and Stefano Quer, To split or to group: from divide-and-conquer to sub-task sharing in verifying multiple properties

Bardh Hoxha, Hoang Bach, Houssam Abbas, Adel Dokhanchi, Yoshihiro Kobayashi and Georgios Fainekos, Towards Formal Specification Visualization for Testing and Monitoring of Cyber-Physical Systems

Registration for the conference is open. Please follow the link. Registration Page.

Information about the venue are available at the following link. Venue.

(rescheduled to synchronize with parallel MEMOCODE sessions)

Workshop Program
8:30-8:50
Breakfast and Registration
8:50-9:00
Welcome
9:00-10:00

1st Invited Talk by Rolf Drechsler, University of Bremen, Germany

Coverage at the Formal Specification Level (Slides)

10:00-10:30
Coffee Break
 
System
10:30-11:00

Alberto Griggio and Marco Roveri

Comparing Different Variants of the IC3 Algorithm for Hardware Model Checking
(Paper) (Slides)

11:00-11:30

Paolo Camurati, Carmelo Loiacono, Paolo Pasini, Denis Patti and Stefano Quer

To split or to group: from divide-and-conquer to sub-task sharing in verifying multiple properties
(Paper) (Slides)

12:00-12:30*

Bardh Hoxha, Hoang Bach, Houssam Abbas, Adel Dokhanchi, Yoshihiro Kobayashi and Georgios Fainekos

Towards Formal Specification Visualization for Testing and Monitoring of Cyber-Physical Systems
(Paper) (Slides)

 
Tools I
11:30-12:00*

Sebastiaan Joosten, Freek Verbeek and Julien Schmaltz

WickedXmas: Designing and Verifying on-chip Communication Fabrics
(Paper) (Slides)

12:30-13:30
Workshop Lunch
13:30-14:20

2nd Invited Talk by Wolfgang Kunz, University of Kaiserslautern, Germany

The big hurdles for FV tools in industrial practice – can we overcome them insystem-level design flows? (Slides)

 
Tools II
14:20-14:50

Daryl Stewart, David Gilday, Daniel Nevill and Thomas Roberts

Processor Memory System Verification using DOGReL: a language for specifying End-to-End properties
(Paper)

14:50-15:20

Tayfun Gezgin, Raphael Weber and Markus Oertel

Multi-aspect Virtual Integration approach for Real-Time and Safety Properties
(Paper) (Slides)

15:20-16:00

3rd Invited Talk by Fahim Rahim, Atrenta Europe, Grenoble, France

Efficiently using formal verification techniques to reduce power

16:00-16:15
Coffee Break
16:15

MEMOCODE final Key Note by Joseph Sifakis

A framework for modeling architectures and their properties

 
DIFTS attendees are invited to attend the MEMOCODE talk
 
 
* Presentations swapped: speaker has conflict with MEMOCODE