SAT Based Design Debugging - Sharad Malik [09:00 - 10:30] Abstract: Propositional Satisfiability (SAT) is seeing increasing use in design verification. One usage scenario involves encoding a verification task as an instance of SAT with the formula representing erroneous conditions. Thus, verification involves proving that this instance is unsatisfiable, i.e., that there are no erroneous conditions. If this is not the case, then a satisfying assignment provides a "counter-example" which can then be used to debug the design. In an alternate use of SAT for design debugging, the specification is inconsistent with the behavior, and therefore yields an inconsistent SAT instance. There are two separate scenarios where such an inconsistency arises. In the first, you have an implementation which does not satisfy its point-wise specification (i.e., test-cases fail). In the second, you have the golden model for the implementation and the observed behavior does not adhere to it. In either scenario, the unsatisfiable SAT instance can then be diagnosed to pin-point the fault. This diagnosis uses the notion of correction sets, which is intimately tied to the notion of unsatisfiable subsets (aka cores) and the MAX-SAT problem. In this tutorial, I will cover design debugging using correction sets and show its application in hardware logic design debugging, software debugging and finally silicon debugging (aka post-silicon validation). Silicon debugging poses difficult challenges due to limited design observability. I will show how the notion of the "backbone" of a satisfiable SAT instance is useful in maximizing information flow in this limited observability context. |
Software Model Checking - Andreas Podelski [11:00 - 12:30] Abstract: Software model checking is an ongoing research topic. We can expect a great number of variations and optimizations to be proposed in the future. Yet, a few basic principles have emerged which will remain the basis for further developments even in the long term. Those few basic principles keep re-appearing in different settings, each setting being motivated by a specific application scenario. The idea of this tutorial is to abstract away from specific application scenarios and to present the few basic principles in the shortest possible way in the simplest possible setting. The tutorial talk will use many examples to explain the basic concepts. It is based on a chapter by Andreas Podelski and Andrey Rybalchenko in the forthcoming Handbook of Model Checking. |
Discretizations based approaches to quantitative verification - P. S. Thiagarajan [14:00 - 15:30] Abstract: Quantitative verification involves the analysis of systems in which the numerical values assumed by one or more real-valued system variables play a vital role in determining the system's behaviour. Timed, hybrid and probabilistic systems are the major varieties of such systems. The formal analysis of such systems is fraught with fundamental difficulties including the fact that many of the interesting behavioural properties are undecidable. We suggest that in these settings finitely discretizing the value domains of the "continuous" variables can often bring significant gains. In particular, while the verification results one obtains are approximate, they can nevertheless be sufficient. We shall illustrate the power of such discretizations in three settings: (i) hybrid automata (ii) ODEs based models of bio-chemical networks and (iii) finite state Markov chains. |