Day 1 - Tuesday, 18 Nov 2014



08:30 - 09:15 Registration

09:15 - 09:30 Opening Remarks,
Moshe Levinger, Area Manager, Computing as a Service, IBM Research - Haifa

09:30 - 10:20 Keynote: SAT Sampling - From Theory to Practice,
Prof. Moshe Vardi, Rice University
Session Chair: Prof. Eran Yahav

Abstract: Counting the number of satisfying truth assignments of a given Boolean formula or sampling such assignments uniformly at random are fundamental computational problems in computer science with numerous applications. In computer-aided design, these problems come up in constrained-random verification, where test input vectors are described by means of constraints. While the theory of these problems has been thoroughly investigated in the 1980s, approximation algorithms developed by theoreticians do not scale up to industrial-sized instances. Algorithms used by the industry offer better scalability, but give up certain correctness guarantees to achieve scalability. We describe a novel approach, based on universal hashing and SMT, that scales to formulas with hundreds of thousands of variables without giving up correctness guarantees.

Joint work with Supratik Chakraborty, Daniel Fremont, Kuldeep Meel, and Sanjit Sheshia.

10:20 - 11:00 Technical Session: Model Checking and Formal Verification 1
Chair: Prof. Moshe Vardi

Combined Bounded and Symbolic Model Checking for Incomplete Timed Systems,
Georges Morbé, Christoph Scholl, Bernd Becker, and Christian Miller

Assume-Guarantee Abstraction Refinement Meets Hybrid Systems,
Sergiy Bogomolov, Goran Frehse, Marius Greitschus, Radu Grosu, Corina Pasareanu, Andreas Podelski, and Thomas Strump

11:00 - 11:30 Break

11:30 - 13:00 Pnueli Memorial Session
Chair: Prof. David Peleg, Weizmann Institute of Science

Memorial words about Amir Pnueli,
Prof. David Harel, Weizmann Institute of Science

From Boolean to Quantitative Methods in Formal Verification,
Prof. Tom Henzinger, IST Austria

Abstract: Formal verification aims to improve the quality of hardware and software by detecting errors before they do harm. At the basis of formal verification lies the logical notion of correctness, which purports to capture whether or not a circuit or a program behaves as desired. We suggest that the Boolean partition into correct and incorrect systems falls short of the practical need to assess the behavior of hardware and software in a more nuanced fashion against multiple criteria. We propose quantitative preference metrics for reactive systems, which can be used to measure the degree of desirability of a system with respect to primary attributes such as function and performance, but also with regard to secondary attributes such as robustness and resource consumption. The theory supports quantitative generalizations of the paradigms that have become success stories in Boolean formal methods, such as temporal logic, property-preserving abstraction, model checking, and reactive synthesis.

Bio: Thomas Henzinger is president of IST Austria (Institute of Science and Technology Austria). He holds a Dipl.-Ing. degree in Computer Science from Kepler University in Linz, Austria, an M.S. degree in Computer and Information Sciences from the University of Delaware, a Ph.D. degree in Computer Science from Stanford University (1991), and a Dr.h.c. from Fourier University in Grenoble, France (2012). He was Assistant Professor of Computer Science at Cornell University (1992-95), Assistant Professor (1996-97), Associate Professor (1997-98), and Professor (1998-2004) of Electrical Engineering and Computer Sciences at the University of California, Berkeley. He was also Director at the Max-Planck Institute for Computer Science in Saarbruecken, Germany (1999) and Professor of Computer and Communication Sciences at EPFL in Lausanne, Switzerland (2004-09). His research focuses on modern systems theory, especially models, algorithms, and tools for the design and verification of reliable software, hardware, and embedded systems. His HyTech tool was the first model checker for mixed discrete-continuous systems. He is an ISI highly cited researcher, a member of Academia Europaea, a member of the German Academy of Sciences (Leopoldina), a member of the Austrian Academy of Sciences, a Fellow of the AAAS, a Fellow of the ACM, and a Fellow of the IEEE. He has received the Wittgenstein Award of the Austrian Science Fund and an ERC Advanced Investigator Grant.

Organized by:
The Faculty of Mathematics and Computer Science
The Weizmann Institute of Science

Sponsored by:
Arthur and Rochelle Belfer Institute of Mathematics and Computer Science

13:00 - 14:30 Lunch

14:30 - 15:20 Keynote: Technology Challenges in Automation of SoC-centric System Verification,
Ziv Binyamini, Cadence
Session Chair: Karen Yorav

Bio: Ziv Binyamini is corporate vice president and CTO in the System and Verification Group at Cadence Design Systems, Inc., where he oversees a team that is providing innovative solutions for emerging SoC verification challenges. Binyamini joined Cadence in 2005 as part of the Verisity acquisition. At Cadence he has led the creation of the OVM and UVM methodologies and the fast growing Cadence Verification IP business.

Binyamini began his career at Intel in 1987 working in Haifa Israel and Portland, Ore., as a CAD engineer and manager. Working on the Pentium Pro design team he developed verification methodologies such as coverage-driven verification, full-chip formal equivalence checking and assertions-driven verification. In 1997 Ziv joined Verisity where he headed the Research and Development team that created Specman® – the industry's first testbench automation product, as well as methodologies such as metric-driven verification and eRM – the industry first verification reuse methodology.

Binyamini holds a Bachelor of Science degree in computer science and mathematics from Bar Ilan University.

15:20 - 16:00 Technical Session: Model Checking and Formal Verification 2
Chair: Karen Yorav

Read, Write, and Copy Dependencies for Symbolic Model Checking,
Jeroen Meijer, Gijs Kant, Stefan Blom, and Jaco van de Pol

Formal Verification of Secure User Mode Device Execution with DMA,
Oliver Schwarz and Mads Dam

16:00 - 16:30 Break

16:30 - 17:50 Technical Session: Solvers
Chair: Prof. Orna Grumberg

Partial Quantifier Elimination,
Eugene Goldberg and Panagiotis Manolios

Reduction of Resolution Refutations and Interpolants via Subsumption,
Roderick Bloem, Sharad Malik, Matthias Schlaipfer, and Georg Weissenbacher

Generating Linear Invariants for Model Checking,
Gadi Aleksandrowicz, Alexander Ivrii, Oded Margalit, and Dan Rasin

A Comparative Study of Incremental Constraint Solving Approaches in Symbolic Execution,
Tianhai Liu, Mateus Borges, Marcelo D'Amorim, and Mana Taghdiri

17:50 - 18:30 Reception

play video


Keynote Speakers

  • Prof. Moshe Vardi, Rice University
  • Wolfgang Roesner, Fellow, IBM
  • Prof. Martin Vechev, ETH Zürich
  • Harry Foster, Chief Verification Scientist, Mentor Graphics
  • Ziv Binyamini, Corporate VP & CTO, System and Software Solutions, Cadence

Previous Conferences

%%sidebarspace%%
See us on Linked In See us on Facebook IBM Research Cadence Mellanox JASPER Qualcomm Mentor Graphics