International Workshop on Design and Implementation of Formal Tools and Systems

Austin, Texas USA, September 26-27, 2015

co-located with FMCAD15, MEMOCODE15, and SAT15

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 FMCAD 2015, MEMOCODE 2015, and SAT 2015. The regular talks of DIFTS workshop will be on September 26, 2015. The full-day tutorial (joint with FMCAD and SAT) will be on September 27, 2015.

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 7, 2015 July 15, 2015.
  • Paper Submission: July 15, 2015 (extended).
  • Author Notification: August 10, 2015.

Program Chairs

Local Arrangement Chair

Program Committee

    Flemming Andersen, Intel, USA

    From Highly Efficient Formal Verification in Selected Areas to Success in an SOC-IP World

    Shobha Vasudevan, UIUC, USA

    Crucial Character Roles for Formal Methods in Contemporary Verification

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.


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.


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).

Registration fees for the DIFTS workshop and co-located conference (FMCAD + Tutorial) are as follows:

Early Registration* Late Registration
DIFTS add-on (with FMCAD and Tutorial) $100 $100
DIFTS + Tutorial (without FMCAD) $250 $300
DIFTS only (without FMCAD and Tutorial) $135 $180

*Early registration ends on September 4, 2015.

Please follow the link: Registration Page.

Conference Location (Direction) (Map)

AT&T Executive Education and Conference Center
1900 University Avenue
Austin, Texas, 78705, USA
+1 512 404 1900

The workshop on Sept 26 will be in Room 202.

Sept 27 : POB, Room 2.302 (Joint tutorial with FMCAD and SAT)

The tutorial on Sept 27 will be held in the POB building on the campus of The University of Texas at Austin.

DIFTS Workshop Program (Sept 26, 2015)
(Room 202, AT&T Center)
Registration and Breakfast

Aina Niemetz, Mathias Preiner, Armin Biere and Andreas Frohlich

Improving Local Search for Bit-Vector Logics in SMT with Path Propagation


Matt Kaufmann and J Strother Moore

Well-Formedness Guarantees for ACL2 Metafunctions and Clause Processors

Coffee Break

Evan Austin and Perry Alexander

Challenges in Implementing an LCF-Style Proof System with Haskell


1st Invited Talk by Flemming Andersen, Intel, USA

From Highly Efficient Formal Verification in Selected Areas to Success in an SOC-IP World

Lunch Break

Robert P. Goldman, David Musliner and Michael Boldt

Heuristic Search for Bounded Model Checking of Probabilistic Automata


Sofia Cassel, Falk Howar and Bengt Jonsson

RALib: A LearnLib extension for inferring EFSMs

Coffee Break

Michael Boldt, Robert Goldman and David Musliner

Offline Monte Carlo Tree Search for Statistical Model Checking of Markov Decision Processes


2nd Invited Talk by Shobha Vasudevan, UIUC, USA

Crucial Character Roles for Formal Methods in Contemporary Verification

Tutorial Day (Sept 27, 2015)
(Room 2.302, POB Building, UT Austin)
joint with FMCAD and SAT
Registration and Breakfast

Andre Platzer , CMU, USA

Tutorial 1: Proving Hybrid Systems
(Speaker Bio)

Coffee Break

Priyank Kalla , University of Utah, USA

Tutorial 2: Formal Verification of Arithmetic Datapaths using Algebraic Geometry and Symbolic Computation
(Speaker Bio)


Roderick Bloem , TU Graz, Austria

Tutorial 3: Reactive Synthesis
(Speaker Bio)

Coffee Break

Isil Dillig , UT Austin, USA

Tutorial 4: Abductive Inference and Its Application in Program Analysis, Verification, and Synthesis
(Speaker Bio)

FMCAD'15 Reception: Scholz Garten