It statically infers a sound -- but not complete --
description of the interactions between the agents of a part of
a system interacting with an unknown context.
(A worst-case semantics describes the context behaviour.)
The description of these interactions are non-uniform which means that recursive instances of processes are distinguished. The prototype allows in proving for instance that:
The prototype "
A short tutorial and few interpreted examples are also given.
A slicing-based tool for identifying duplicated code in C programs Abstract: This is a tool that uses a program dependence graph (PDG) representation of programs, and a variation of the technique of backward slicing, to find duplicated code in C programs. The key benefits of this novel approach is that the tool is able to find non-contiguous fragments of duplicated code, and other kinds of inexact matches. This tool is described further in the SAS '01 paper titled "Using Slicing to Identify Duplication in Source Code" co-authored by Raghavan Komondoor and Susan Horwitz.
Abstract interpretation of probabilistic programs Abstract: We demonstrate a little tool that analyzes programs written in a subset of C that can make use of probabilistic and nondeterministic choice operators and computes safe bounds on the probabilities of outcomes. A symbolic and a statistical analyses are implemented.
LOOP, a localised analyser for object-oriented programs. Abstract: LOOP, is a localised analyser for object-oriented programs, based on the watchpoint semantics presented at the SAS'01 conference. More information about LOOP is available here
A New Model-Checker for Real-Time Systems based on BDD-like data-structures. Abstract: New version 3.1 of RED is implemented with the new data-structure of CRD (Clock-Restriction Diagram), which is a BDD-like data-structure for the representation of dense-time state-space. for the TCTL model-checking of timed automata with counter-example generating capability. Efficient CRD manipulation depends heavily on the succinctness of CRD. In addition to dense-time clocks, RED 3.0 also supports the verification of systems with pointer data-structures and synchronizers. In this demonstration, we explain the idea of CRD and run several experiments.