DIFTS15

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.

DIFTS11 (Austin, Texas, USA)
DIFTS13 (Portland, Oregon, USA)
DIFTS14 (Lausanne, Switzerland)

Program Chairs

Malay K. Ganai, Synopsys, Inc., USA
Chao Wang, Virginia Tech, USA

Local Arrangement Chair

Adnan Aziz, UT Austin, USA

Program Committee

Erika Abraham, RWTH Aachen University, Germany
Malay K. Ganai, Synopsys, Inc., USA
Alberto Griggio, FBK-IRST, Italy
Daniel Grosse, University of Bremen, Germany
William Hung , Synopsys, Inc., USA
Priyank Kalla, University of Utah, USA
Joao Marques-Silva, University College Dublin, Ireland
Sandip Ray , Intel Corporation, USA
Alper Sen, Bogazici University, Turkey
Andreas Veneris, University of Toronto, Canada
Chao Wang, Virginia Tech, USA

Flemming Andersen, Intel, USA

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

Abstract

Shobha Vasudevan, UIUC, USA

Crucial Character Roles for Formal Methods in Contemporary Verification

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

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)
8:00-9:00	Registration and Breakfast
9:00-9:15	Welcome
	System
9:15-9:45	Aina Niemetz, Mathias Preiner, Armin Biere and Andreas Frohlich Improving Local Search for Bit-Vector Logics in SMT with Path Propagation (Paper) Abstract Bit-blasting is the main approach for solving word-level constraints in SAT Modulo Theories (SMT) for bit-vector logics. However, in practice it often reaches its limits, even if combined with sophisticated rewriting and simplification techniques. In this paper, we extended a recently proposed alternative based on stochastic local search (SLS) and improve neighbor selection based on down propagation of assignments. We further reimplemented the previous SLS approach in our SMT solver Boolector and confirm its effectiveness. We then added our novel propagation-based extension and provide an extensive experimental evaluation, which suggests that combining these techniques with Boolector’s bit-blasting engine enables Boolector to solve substantially more instances.
9:45-10:15	Matt Kaufmann and J Strother Moore Well-Formedness Guarantees for ACL2 Metafunctions and Clause Processors (Paper) Abstract Some runtime checks can be safely removed from code if appropriate program properties are proved. We describe how we have applied this idea to the ACL2 theorem prover to speed up the application of user-defined proof procedures. In particular, we discuss how and why we have added a new feature to ACL2 that allows the user to verify certain well-formedness proper- ties of the expressions produced by user-defined proof procedures. Of special interest are the is- sues of extensibility (how we know that guaran- tees proved in one theory are adequate in an- other), formalization of the problem, and design decisions affecting the user interface.
10:15-10:30	Coffee Break
10:30-11:00	Evan Austin and Perry Alexander Challenges in Implementing an LCF-Style Proof System with Haskell (Paper) Abstract The predominant, root design among current proof assistants, the LCF style, is traditionally realized through impure, functional languages. Thus, languages that eschew side-effects in the name of purity collectively represent a largely untapped platform for exploring alternate implementations of LCF-style provers. The work in this paper details the challenges we have encountered in the development of one such implementation, a monadic approach to the LCF style tailored to the Haskell programming language. The resultant proof system, HaskHOL, is introduced and our current work with it is briefly discussed.
11:00-12:00	1st Invited Talk by Flemming Andersen, Intel, USA From Highly Efficient Formal Verification in Selected Areas to Success in an SOC-IP World (Bio) Abstract Over the past twenty years the hardware industry gained a lot of experience with practical application of formal methods- and verification. From originally being able to formally verify only RTL components with hundreds of gates, the tools today supports millions of gates. In addition, experience indicates that a combination of functional equivalence verification techniques combined with assertion based temporal logic verification of control logic is required to efficiently handle the size, functionality, and complexity of design components today. The most successful application areas have naturally been those like arithmetic, decoders/encoders, cache coherence protocols, RAS/ECC, and other areas where solid standards such as the IEEE 754 floating point standard rigorously define what the formal specifications should be. Areas where no standards are given, keep on being a challenge for formal verification since the investment in specifications are often more or less useless when the next product is being developed. Hence, the introduction of IP-components and sub-systems with standardized interfaces- and protocols to develop SOC products enables much stronger use of formal methods- and verification if used correctly. In this presentation we will look at different successful formal verification areas and discuss how these can be used as a model- and method for success in an SOC-IP world.
12:00-14:00	Lunch Break
	Tools
14:00-14:30	Robert P. Goldman, David Musliner and Michael Boldt Heuristic Search for Bounded Model Checking of Probabilistic Automata (Paper) Abstract We describe a new method for bounded model-checking of probabilistic automata (PAs), based on heuristic search and integrated into the PRISM model-checker. PA models include both probabilistic transitions and nondeterministic choice transitions. Our search-based approach aims to address weaknesses in statistical and dynamic-programming approaches to checking bounded PCTL properties of probabilistic automata. To model-check properties of PA models, we must demonstrate that the property will be satisfied even in the face of an adversary that optimally resolves nondeterministic choices. We use heuristically guided AO* search to find the optimal adversary policy and estimate the probability of properties. We adapt techniques from Artificial Intelligence Planning to develop a heuristic that is based on a relaxation of the underlying probability model. This heuristic provides critical guidance to the search algorithm: without it, even very small models are unsolvable. We have implemented our algorithm in the PRISM model-checker, and show cases where it outperforms PRISM’s dynamic programming methods. We also describe promising directions for future work in search-based PA model-checking, notably introducing further abstraction into the heuristic to address memory issues.
14:30-15:00	Sofia Cassel, Falk Howar and Bengt Jonsson RALib: A LearnLib extension for inferring EFSMs (Paper) Abstract Active learning of register automata infers extended finite state machines (EFSMs) with registers for storing values from a possibly infinite domain, and transition guards that compare data parameters to registers. In this paper, we present RALib, an extension to the LearnLib framework for automata learning. RALib provides an extensible implementation of active learning of register automata, together with modules for output, typed parameters, mixing different tests on data values, and directly inferring models of Java classes. RALib also provides heuristics for finding counterexamples as well as a range of performance optimizations. Compared to other tools for learning EFSMs, we show that RALib is superior with respect to expressivity, features, and performance.
15:00-15:30	Coffee Break
15:30-16:00	Michael Boldt, Robert Goldman and David Musliner Offline Monte Carlo Tree Search for Statistical Model Checking of Markov Decision Processes (Paper) Abstract To find the optimal policy for large Markov Decision Processes (MDPs), where state space explosion makes analytic methods infeasible, we turn to statistical methods. In this work, we apply Monte Carlo Tree Search to learning the optimal policy for a MDP with respect to a Probabilistic Bounded Linear Temporal Logic property. After we have the policy, we can proceed with statistical model checking or probability estimation for the property against the MDP. We have implemented this method as an extension to the PRISM probabilistic model checker, and discuss its results for several case studies.
16:00-17:00	2nd Invited Talk by Shobha Vasudevan, UIUC, USA Crucial Character Roles for Formal Methods in Contemporary Verification (Bio) Abstract In this talk, I will present the script that stars formal methods not in the lead roles, but in character roles that are seminal to the storyline. I will narrate this success story in two parts. In the first part, I will talk about GoldMine, a suite of algorithms for automatic assertion generation that use a combination of machine learning and formal analysis. I will discuss our methods for assertion evaluation as an allied topic to demonstrate the goodness of the GoldMine solution. I will also outline briefly the widespread applicability of the "GoldMine principle", or the combination of formal model based analysis with data driven, statistical methods in many fields like debugging, diagnostics and data analytics. In the second part, I will talk about a set of analog and mixed signal validation methods that provide value and efficiency over traditional Monte Carlo simulations. These methods are based on rigorous geometric analysis combined with simulation methods from robot motion planning. I will discuss worst case behavior or "eye diagram" analysis and analog test compaction as the applications of this technology. I will conclude by highlighting the importance of formal methods and strategic ways to scale them in an "oscar winning" performance.

Tutorial Day (Sept 27, 2015) (Room 2.302, POB Building, UT Austin) joint with FMCAD and SAT
8:00-9:00	Registration and Breakfast
9:00-10:15	Andre Platzer , CMU, USA Tutorial 1: Proving Hybrid Systems (Speaker Bio) Abstract Cyber-physical systems (CPS) combine cyber aspects such as communication and computer control with physical aspects such as movement in space, which arise frequently in many safety-critical application domains, including aviation, automotive, railway, and robotics. But how can we ensure that these systems are guaranteed to meet their design goals, e.g., that an aircraft will not crash into another one? This tutorial focuses on the most elementary CPS model: hybrid systems, which are dynamical systems with interacting discrete transitions and continuous evolutions along differential equations. It describes a compositional programming language for hybrid systems and shows how to specify and verify correctness properties of hybrid systems in differential dynamic logic. Extensions of this logic that support CPS models with more general dynamics will be surveyed briefly. In addition to providing a strong theoretical foundation for CPS, differential dynamic logics have also been instrumental in verifying many applications, including the Airborne Collision Avoidance System ACAS X, the European Train Control System ETCS, several automotive systems, mobile robot navigation with the dynamic window algorithm, and a surgical robotic system for skull-base surgery. The approach is implemented in the theorem prover KeYmaera X.
10:15-10:30	Coffee Break
10:30-11:45	Priyank Kalla , University of Utah, USA Tutorial 2: Formal Verification of Arithmetic Datapaths using Algebraic Geometry and Symbolic Computation (Speaker Bio) Abstract Here is the PDF of the abstract.
11:45-14:00	Lunch
14:00-15:15	Roderick Bloem , TU Graz, Austria Tutorial 3: Reactive Synthesis (Speaker Bio) Abstract Synthesis is the question of how to construct a correct system from a specification. In recent years, synthesis has made major steps from a theoretist’s dream towards a practical design tool. While synthesis from a language like LTL has very high complexity, synthesis can be quite practical when we are willing to compromise on the specification formalism. Similarly, we can take a pragmatic approach to synthesize small distributed systems, a problem that is in general undecidable.
15:15-15:45	Coffee Break
15:45-17:00	Isil Dillig , UT Austin, USA Tutorial 4: Abductive Inference and Its Application in Program Analysis, Verification, and Synthesis (Speaker Bio) Abstract Abductive inference is a form of backwards logical reasoning that infers likely hypotheses from a given conclusion. In other words, given an invalid implication of the form A => B, abduction asks the question "What formula C do we need to conjoin with the antecedent A so that (i) A & C => B is logically valid and (ii) C is consistent with A?" Abductive reasoning has found many applications in program verification and synthesis, particularly in modular program analysis, invariant generation, and automated inference of missing program expressions. This tutorial will give an overview of logical abduction and algorithms for performing abductive inference. We will also survey several use cases of abductive inference in the context of program analysis, verification, and synthesis.
19:00	FMCAD'15 Reception: Scholz Garten

DIFTS15

Sponsored by

Call for Papers

Workshop Scope

Topics of Interest

Important Dates

Past Workshops

Committees

Program Chairs

Local Arrangement Chair

Program Committee

Invited Speakers

Flemming Andersen, Intel, USA

Shobha Vasudevan, UIUC, USA

Paper Submission

Evaluation

Publication

Registration

Venue

Program