| SVV 06 | International Workshop on Software Verification and Validation Seattle, August 21, 2006 |
SVV on Monday, August 21st
Session 1: Invited Talk (09:15‑10:30)
Break (10:30‑11:00)
Session 2 (11:00‑12:00)
| 11:00‑11:30 | Ganna Zaks
(New York University) Amir Pnueli (New York University) Translation Validation of Interprocedural Optimizations Translation Validation is an approach of ensuring compilation correctness in which each compiler run is followed by a validation pass that proves that the target code of the program produced by the compiler is a correct translation (implementation) of the source code. In this work, we extend the existing framework for translation validation of optimizing compilers to deal with procedural programs and define the notion of correct translation for reactive programs with intermediate inputs and outputs. We present an Interprocedural Translation Validation algorithm that automatically proves correct translation of the source program to the target program in presence of interprocedural optimizations such as global constant propagation, interprocedural dead code elimination, dead argument elimination, inlining, cloning, and tail-recursion elimination. |
| 11:30‑12:00 | Luke Simon (University of Texas at Dallas) Ajay Mallya (University of Texas at Dallas) Ajay Bansal (University of Texas at Dallas) Gopal Gupta (University of Texas at Dallas) Co-Logic Programming: Extending Logic Programming with Coinduction Traditional logic programming with its minimal Herbrand model semantics is useful for declaratively defining finite data structures and properties, while coinductive logic programming allows for logic programming with infinite data structures and properties. In this paper we present the theory and practice of it co-logic programming} (co-LP for brevity), a paradigm that combines both inductive and coinductive logic programming. Co-LP allows predicates to be annotated as coinductive; by default, unannotated predicates are assumed to be inductive. Coinductive predicates can call inductive predicates and vice versa, the only exception being that no cycles are allowed through alternating calls to inductive and coinductive predicates. Co-LP is a natural generalization of logic programming and coinductive logic programming, which in turn generalizes other extensions of logic programming, such as infinite trees, lazy predicates, and concurrent communicating predicates. The declarative semantics for co-LP is defined, and a corresponding top-down, goal-directed operational semantics is provided in terms of alternating SLD and co-SLD semantics. Co-LP has applications to rational trees, verifying infinitary properties, lazy evaluation, concurrent logic programming, model checking, bisimilarity proofs, Answer Set Programming (ASP), etc.; some of these applications are discussed in this paper. An outline of a prototype implementation realized by modifying YAP Prolog's engine at the WAM level is also described. |
Lunch break (12:30‑14:00)
Session 3 (14:00‑15:30)
| 14:00‑14:30 | Aleks Zaks (New York University) Ilya Shlyakhter (NEC Laboratories USA) Franjo Ivancic (NEC Laboratories USA) Srihari Cadambi (NEC Laboratories USA) Zijiang Yang (Western Michigan University) Malay Ganai (NEC Laboratories USA) Aarti Gupta (NEC Laboratories USA) Pranav Ashar (Real Intent) Using Range Analysis for Software Verification Verification is increasingly becoming a bottleneck in the design of embedded systems and system-on-chips. In order to ensure the correctness, verification has to be performed not only on hardware, but also on software. Model checking is a promising verification technique, but suffers from the state explosion problem, which is even further exacerbated in the context of software verification mainly due to large number of variables used in programs. Therefore, how to reduce the amount of variables during verification becomes a key challenge in making software model checking scalable. The main contributions of this paper are two light-weight range analysis techniques for determining lower and upper bounds for program variables, and their application in improving various software model checking techniques. We formulate each range analysis problem as a system of inequality constraints between symbolic bound polynomials, then reduce the constraint system to a linear program (LP) that can be analyzed by available LP solvers. For bounded model checking, we improve the bound tightness by exploiting the fact that the range information needs to be sound only for bounded traces. We have implemented the range analysis techniques in our software model checking framework. Experimental results demonstrate promising results in extending the power of state-of-the-art software verification techniques. |
| 14:30‑15:00 | Elvira Albert
(Complutense University of Madrid) Miguel Gómez-Zamalloa (Complutense University of Madrid) Laurent Hubert (Technical University of Madrid) German Puebla (Technical University of Madrid) Java Bytecode Verification using Analysis and Transformation of Logic Programs State of the art analyzers in the (Constraint) Logic Program- ming paradigm (or (C)LP for short) are nowadays mature and sophisti- cated. They allow inferring a wide variety of global properties including termination, run-time error freeness, bounds on resource consumption, etc. The aim of this work is to automatically transfer the power of such analysis tools for LP to the analysis and verification of Java bytecode. In order to achieve our goal, we rely on well-known techniques for meta- programming and program specialization. More precisely, we propose to partially evaluate a Java bytecode interpreter implemented in LP w.r.t. (a LP representation of ) a set of Java bytecode classes and then an- alyze the residual program. Interestingly, at least for the examples we have studied, our approach produces very simple LP representations of the original Java bytecode programs. This can be seen as an automatic translation and decompilation from Java bytecode to LP source. Rea- soning about properties of such residual programs allows automatically proving some non-trivial properties of Java bytecode programs such as termination and run-time error freeness. |
| 15:00‑15:30 | Stefano Tonetta (University of Lugano) Natasha Sharygina (UNISI) A Uniform Framework for Predicate Abstraction Approximation Abstraction refinement is a powerful technique that enables the verification of real systems. An initial coarse abstraction is provided and iteratively refined until either the property is proved to be true or false. Computing a precise abstraction is usually very expensive. Thus, many techniques have been conceived in order to approximate the abstract transition relation. In the framework of predicate abstraction, examples of such techniques are early quantification, Cartesian approximation, maximum cube length approximation, predicate partitioning, and interpolation-based approximation. When such approximations are employed, adding new predicates is no more sufficient to rule out all spurious counterexamples. Standard model checkers add new constraints to the transition relations in order to refine the approximation. We propose a uniform framework for describing most of known approximation techniques. The mapping among various techniques provides a conceptual basis for the development of new algorithms. |
Break (15:30‑16:00)
Session 4 (16:00‑17:00)
