First International Workshop on Numerical Abstractions for Software Verification.

July 8th, 2008.

Affliated with CAV 2008

Venue: Princeton, NJ

Infinite State Model Checking Using Presburger Arithmetic

Model checking was originally conceived as a finite state verification technique. It is possible to extend symbolic model checking to infinite domains using symbolic representations that encode infinite sets. Action Language Verifier is an infinite-state model checker built on top of a symbolic manipulator called Composite Symbolic Library. Composite Symbolic Library combines different symbolic representations, such as BDDs for representing boolean logic formulas and polyhedral or automata-based representations for Presburger arithmetic formulas, using a disjunctive composite representation.

Since infinite state model checking is undecidable in general, fixpoint computations in an infinite state symbolic model checker are not guaranteed to converge. Using conservative approximations one can force termination of the fixpoint computations. When such approximations are used, in some cases, the model checker may not be able to verify or falsify a property. Several heuristics can be used to reduce the occurrence of such cases.

After giving an overview of the infinite state model checking techniques used in Action Language Verifier, I will discuss their application to verification of synchronization in concurrent programs based on a design for verification approach.

Translation Validation of Generated Code in the Context of IEC61508

Mirko Conrad, MathWorks Inc., USA

Abstract:

Production code generation with Model-Based Design has successfully replaced manual coding across various industries and application domains. Furthermore, generated code is increasingly being deployed in embedded safety-related applications. To validate the model-to-code translation process as well as to ensure quality and functional safety, generated software components and its precursory stages shall be subjected to a combination of quality assurance measures. Further, compliance with safety standards such as IEC 61508 needs to be demonstrated.

On principle, translation validation of generated code could be carried out in the same manner as for hand code. However, this would not leverage the advantages of Model-Based Design and w.r.t process efficiency this would leave something to be desired. Therefore, engineering methods and tools for the translation validation of generated code are highly desirable. As a step towards this goal, a workflow for verification and validation of models and generated code will proposed and as far as possible mapped onto the objectives of IEC 61508-3. A core activity within this workflow is testing for numerical equivalence between models and generated code.

Proving recursive programs terminating, without the recursion

Byron Cook, Microsoft Research Labs, Cambridge, UK.

Numerical Domains for Software Verification By Abstract Interpretation

Patrick Cousot, ENS, France

Abstract:

Abstract interpretation allows the automatic inference of numerical and symbolic invariants about program behaviors. The nature of the invariants is captured by fixpoint inference using a combination of abstract domains. We discuss and compare integer, real and floating-point numerical abstractions used in software verification by abstract interpretation. The considered abstractions extend from simple non-relational ones to more complex relational linear or non-linear abstractions. The six central issues to be considered are:

• adequacy of the concrete semantics (choice of primitives, mathematical versus computer-based definition, etc),
• nature of the abstraction (relational, non-relational, parametric, etc.) and its computer encoding,
• soundness of the abstraction and the abstract verification conditions (so that no later inference can lead to erroneous conclusions such as false positives),
• correct and effective induction (that is how inductive invariants are computed by concrete/abstract iteration with extrapolation, constraint solving, abstraction/refinement, elimination, exact resolution, etc),
• ability to scale up (for programs in the small to programs in the large, separate abstractions, etc), and
• precision of the abstraction (to avoid false alarms).

In conclusion we discuss the limitations restraining the practical use of the currently available abstractions and how they could be overcome.

Automatically Refining Abstract Interpretations

Sriram Rajamani, Microsoft Research Labs, Bangalore, India.

Abstract:

Abstract interpretations are used to prove properties about programs. These techniques are produce sound over-approximations of program behavior, but are prone to false errors. Counter-example driven refinement techniques for predicate abstraction (which is a particular abstract interpretation) has been used to reduce false errors in tools like SLAM. Inspired by the success of these tools, we present approaches to refine any abstract interpretation automatically using counterexamples. Several challenges arise: refining using disjunctions leads to powerset domains, and the use of joins forces us to consider counterexample DAGs instead of counterexample traces. We present our solutions to these problems. We also present experiences implementing our techniques in a tool DAGGER.

(joint work with Bhargav Gulavani, Supratik Chakroborty and Aditya Nori)

Using the Theory of Reals in Analyzing Continous and Hybrid Systems

Ashish Tiwari , SRI International, USA.

Abstract:

Hybrid systems is a powerful language for modeling systems that exhibit dynamics at vastly different time scales, such as embedded control systems and biological systems. Since real numbers are an integral part of the description of a hybrid system, verification and analysis of hybrid systems depends crucially on the ability to reason about numbers.

This talk will presents results and techniques in the area of continuous and hybrid system verification that depend crucially on the ability to reason about numerical constraints. The theory of reals has been used to not only obtain decidability results but also practical techniques to generate invariants and prove safety of continuous and hybrid systems.

Modular Code Generation from Synchronous Block Diagrams

Stavros Tripakis, Cadence, USA and Verimag, France.

Abstract:

We study modular, automatic code generation from hierarchical block diagrams with synchronous semantics. Such diagrams are the fundamental model behind widespread tools such as Simulink and SCADE. Modularity means code is generated for a given composite block independently from context, that is, without knowing in whih diagrams this block is going to be used. This can be achieved by abstracting a given macro (i.e., composite) block into a set of interface functions plus a set of dependencies between these functions. These two pieces of information form the exported interface for a block. An implementation of the interface functions constitutes an implementation of this interface.

This approach allows modularity to be quantified, in terms of the size of the interface, that is, the number of interface functions that are generated per block. The larger this number, the less modular the code is. This definition reveals a fundamental trade-off between modularity and reusability (set of diagrams the block can be used in): using an abstraction that is too coarse (i.e., too few interface functions) may create false input-output dependencies and result in dependency cycles due to feedback loops. We explore this and other trade-offs. We also report on a prototype tool and results obtained by using the tool on realistic case studies from the Simulink demo suite.