Tutorials
| Speaker | Affiliation | Tutorial Title |
| Armin Biere | Johannes Kepler University, Linz | Challenges in Bit-Precise Reasoning |
| Morgan Deters Andrew Reynolds Timothy King Clark Barrett Cesare Tinelli |
New York University and University of Iowa |
A Tour of CVC4: How it works, and how to use it |
| Ziyad Hanna | Cadence Design Systems | Challenging Problems in Industrial Formal Verification |
| Johannes Kinder | Royal Holloway, University of London | Efficient Symbolic Execution for Software Testing |
Abstracts
Title: Challenges in Bit-Precise ReasoningSpeaker: Armin Biere
Day: Tuesday, October 21, 2014
Bit-precise reasoning (BPR) precisely captures the semantics of systems down to each individual bit and thus is essential to many verification and synthesis tasks for both hardware and software systems. As an instance of Satisfiabiliy Modulo Theories (SMT), BPR is in essence about word-level decision procedures for the theory of bit-vectors. In practice, quantiers and other theory extensions, such as reasoning about arrays, are important too. In the first part of the tutorial we gave a brief overview on basic techniques for bit-precise reasoning and then covered more recent theoretical results, including complexity classification results. We discussed challenges in developing an efficient SMT solver for bit-vectors, like our award winning SMT solver Boolector, and in particular presented examples, for which current techniques fail. Finally, we reviewed the state-of-the-art in word-level model checking, and argued why it is necessary to put more effort in this direction of research.
Title: Challenging Problems in Industrial Formal Verification
Speaker: Ziyad Hanna
Day: Tuesday, October 21, 2014
The electronic design industry has emerged in the recent years to adopt the system-on-chip (SoC) design methodology, where systems become a smart and complex integration of many configurable and reusable intellectual properties (IP) designs such as CPU, GPU, DSP, etc. SoC design methodologies have become common to a wide range of systems, starting from high-end servers, down to tablets, smartphones, Internet-of-things and wearable devices. The aggressive time-to-market and the hard competition add a major challenge to the electronic design companies to deliver high volume, and high quality products. Integration and validation of such designs has become the major challenge. The EDA industry and the academia has continued the innovation pipeline trying to cope with the complexity of such systems however major challenges are still ahead. Formal verification has emerged in the recent years to become a mainstream technology in SoC/IP design and verification methodologies. In the past, the usage of formal verification was limited to a small range of applications and it was mainly for verifying complex protocols, or some tricky logic functionality by formal experts. However in the recent years,we see a rapid adoption of formal, and we see a widespread of formal verification applications for low power design, security, SoC connectivity, configuration status register, and many more. In this talk, we provide an overview of the challenges that we see in designing SoC systems and configurable IPs, and provide some ideas to stimulate the academic research, aiming at increasing the research and innovation in such areas for keeping bridging the emerging gap that the electronic design industry is facing now and will face in the future.
Title: A Tour of CVC4: How it works, and how to use it
Speaker(s): Morgan Deters, Andrew Reynolds, Timothy King, Clark Barrett, Cesare Tinelli
Day: Tuesday, October 21, 2014
CVC4 is a solver for Satisfiability Modulo Theories (SMT). This tutorial aims to give participants an overview of SMT, describe the main features of CVC4, and walk through in-depth examples using CVC4 to demonstrate how to solve real problems with an SMT solver. We will provide a detailed description of various aspects of CVC4's internals, including its architecture, its capacity for dealing with quantifiers, its finite model finder, and the linear arithmetic solver. We will show examples of software and hardware verification problems, and how they are encoded and handled by these features in CVC4.
Participants are expected to have only a basic knowledge of what SMT is. This tutorial will give casual users a taste of encoding complex, real-world problems in SMT and effectively using CVC4 to solve them. Participants will be left with some knowledge of what goes on inside a modern SMT solver and some of the practical issues that arise in using them.
CVC4, jointly developed at New York University and the University of Iowa, is freely available for both research and commercial use under an open-source license. The organizers of this tutorial are all architects and implementors of CVC4 and have extensive expertise in the area of SMT.
Title: Efficient Symbolic Execution for Software Testing
Speaker: Johannes Kinder
Day: Tuesday, October 21, 2014
Symbolic execution has proven to be a practical technique for building automated test case generation and bug finding tools. While the basic technique had been introduced already in the 70s, the advent of modern SAT and SMT solvers has lead to a surge of tools and techniques in the area over the last decade. This tutorial will introduce and compare the different approaches to using symbolic execution for testing and discuss the specific challenges and trade-offs. A main challenge in symbolic execution is path explosion, and various proposals have been made to either combat it. I will discuss how these techniques affect the number and type of solver queries that have to be made, and how this can lead to surprising effects on the efficiency of a symbolic execution engine. Going further, we will look at developments to increase the scope of symbolic execution to larger software systems. Specific topics covered include state merging, procedure summaries, abstraction, search strategies, and parallelization.