Date: Wednesday 26 March 2014
Time: 08:30 - 10:00
Location / Room: Konferenz 3
Chair:
Fahim Rahim, Atrenta, FR
Co-Chair:
Bernd Becker, University of Freiburg, DE
While the industrial usage of formal methods has proliferated in the past decade, the capacity limitations of these techniques remains a challenge to their applicability. This session introduces a set of novel advances to boost the scalability of numerous state-of-the-art verification core technologies.
| Time | Label | Presentation Title Authors |
|---|---|---|
| 08:30 | 5.5.1 | SCALABLE LIVENESS VERIFICATION FOR COMMUNICATION FABRICS Speakers: Sebastiaan Joosten and Julien Schmaltz, Open University, NL Abstract In the realm of multi-core processors and systems-on-chip, communication fabrics constitute a key element. A large number of queues and distributed control are two important aspects of this class of designs. These aspects make decomposition and abstraction techniques difficult to apply. For this class of designs, the application of formal methods is a real challenge. In particular, the verification of liveness properties is often intractable. Communication fabrics can be seen as a set of queues and flops interconnected by combinatorial logic. Based on this simple but powerful observation, we propose a novel method for liveness verification. Our method directly applies to Register Transfer Level designs. The essential aspects of our approach are (1) to abstract away from the details of queue implementations and (2) an efficient encoding of liveness properties in an SMT instance. Experimental results are promising. Designs with hundreds of queues can be analysed for liveness within minutes. |
| 09:00 | 5.5.2 | PROPERTY DIRECTED INVARIANT REFINEMENT FOR PROGRAM VERIFICATION Speakers: Tobias Welp1 and Andreas Kuehlmann2 1UC Berkeley, US; 2Coverity, Inc., US Abstract We present a novel, sound, and complete algorithm for deciding safety properties in programs with static memory allocation. The new algorithm extends the program verification paradigm using loop invariants with a counterexample guided abstraction refinement (CEGAR) loop where the refinement is achieved by strengthening loop invariants using the QF\_BV generalization of Property Directed Reachability (PDR). We compare the algorithm with other approaches to program verification and report experimental results. |
| 09:30 | 5.5.3 | SIMPLE INTERPOLANTS FOR LINEAR ARITHMETIC Speakers: Christoph Scholl1, Florian Pigorsch1, Stefan Disch1 and Ernst Althaus2 1University Freiburg, DE; 2University Mainz, DE Abstract Craig interpolation has turned out to be an essential method for many applications in formal verification. In this paper we focus on the computation of simple interpolants for the theory of linear arithmetic with rational coefficients. We successfully minimize the number of linear constraints in the final interpolant by several methods including proof transformations, linear programming, and SMT solving. Experimental results comparing the approach to standard methods from the literature prove the effectiveness of the approach and show reductions of up to 70% in the number of linear constraints. |
| 09:45 | 5.5.4 | TIGHTENING BDD-BASED APPROXIMATE REACHABILITY WITH SAT-BASED CLAUSE GENERALIZATION Speakers: Gianpiero Cabodi, Paolo Pasini, Stefano Quer and Danilo Vendraminetto, Politecnico di Torino, IT Abstract In the framework of symbolic model checking, BDD-based approximate reachability is potentially much more scalable than its exact counterpart. However, its practical applicability is highly limited by its static approach to abstraction, and the intrinsic difficulty to find an acceptable trade-off between accuracy and (memory/time) complexity. In this paper, we explore the use of CNF clauses, and of recent improvements in SAT algorithms, as additional players in BDD-based reachability. Cube generalization, a core step of the IC3 model checking algorithm, is the process of finding a minimal sub-clause, by removing as many literals as possible, such that it over-approximates a set of reachable states while excluding the cube. Generalization is used in IC3 to refine clause-based representations of state sets. We use it, in both the inductive and non inductive version, in order to strengthen BDD-based representations of state sets, computed by Machine By Machine (MBM) and Frame By Frame (FBF) over-approximate forward traversal algorithms. The resulting approach benefits from the orthogonal power of BDD and CNF representations, and it improves the scalability of BDD-based methods. Preliminary experimental results confirm that this approach can provide tighter representations of reachable state sets. Applications include fully BDD-based engines, as well as using over-approximate state sets as invariants or constraints in SAT-based model checking. |
| 10:00 | IP2-16, 831 | MAKE IT REAL: EFFECTIVE FLOATING-POINT REASONING VIA EXACT ARITHMETIC Speakers: Miriam Leeser1, Saoni Mukherjee1, Jaideep Ramachandran1 and Thomas Wahl2 1Northeastern University, US; 2Northeastern University, Boston, US Abstract Floating-point arithmetic is widely used in scientific computing. While many programmers are subliminally aware that floating-point numbers only approximate the reals, few are cognizant of the dangers this entails for programming. Such dangers range from tolerable rounding errors in sequential programs, to unexpected, divergent control flow in parallel code. To address these problems, we present a decision procedure for floating-point arithmetic (FPA) that exploits the proximity to real arithmetic (RA), via a lossless reduction from FPA to RA. Our procedure does not involve any form of bit-blasting or bit-vectorization, and can thus generate much smaller back-end decision problems, albeit in a more complex logic. This tradeoff is beneficial for the exact and reliable analysis of parallel scientific software, which tends to give rise to large but benignly structured formulas. We have implemented a prototype decision engine and present encouraging results analyzing such software for numerical accuracy. |
| 10:00 | End of session Coffee Break in Exhibition Area On Tuesday-Thursday the coffee and lunch breaks will be located in the Exhibition Area (Terrace Level). |