CAVERN
ANR-07-SESUR-003
http://www-anr-ci.cea.fr
Sécurité et Sûreté Informatique
Cpbpv (CeP) is a novel constraint-programming framework for bounded program verification. The Cpbpv framework
uses constraint stores to represent the specification and the program and explores execution paths non-deterministically.
The input program is partially correct if each constraint store so produced implies the post-condition. Cpbpv does
not explore spurious execution paths as it incrementally prunes execution paths early by detecting that the
constraint store is not consistent. Cpbpv is parameterized with a list of solvers which are tried in sequence,
starting with the least expensive and less general. Experimental results often produce orders of magnitude
improvements over earlier approaches, running times being often independent of the variable domains. Moreover,
Cpbpv was able to detect subtle errors in some programs while other frameworks based on model checking have failed.
Euclide (INRIA-Lande) is a Constraint-Based Testing tool for verifying
safety-critical C programs. By using a mixture of symbolic and numerical analyses
(namely static single assignment form, constraint propagation, integer linear relaxation and search-based
test data generation),
it addresses three distinct applications in a single framework: structural
test data generation, counter-example generation and partial program proving.
The core algorithm of the tool takes as input a C program and a point to reach somewhere in the code. As a result, it outcomes
either a test datum that reaches the selected point, or an ``unreachable'' indication showing that the
selected point is unreachable. Optionally, the tool takes as input additional safety properties that can be
given under the form of pre/post conditions in ACSL or assertions directly written in the code.
In this case, Euclide can either prove that these
properties or assertions are verified or find a counter-example when there is one. As these problems are undecidable
in the general case, Euclide only provides
a semi-correct procedure (when it terminates, it provides the right answer) for them.
Current Research works around the tool focus on modular integers and floating-point computations and better
constraint solving procedures based on relational abstract domains computations.
Gatel (CEA) is a test environment for synchronous models of reactive systems
described in Lustre/SCADE. The core of the tool is a CLP interpretation
of the Lustre language, together with a resolution procedure dedicated to
the underlying linear temporal logic. This framework allows to automate a
wide range of usual testing activities. Initially designed for generating
test sequences according to a test objective, Gatel also addresses symbolic
simulation, model debug, conformance checking, coverage analysis/completion,
test suite evaluation. Current work is twofold: updating the CLP
interpretation and procedure to the latest version of the SCADE Suite
(enriched with built-in state machines), upgrading the procedure with
powerful abstractions to scale up to real-life industrial models.
Jaut (Java Automatic Unit Testing) (INRIA -- Lande) is a test case generator for programs in bytecode
Java. Given a bytecode instruction of the method under test, it aims to find an input memory state (values of
the parameters and of the instances in the heap) to cover this instruction. Repeating this process, the
structural coverage criteria of all-the-statements can be fulfilled. In Jaut, bytecode instructions
are modelled with constraints, as well as the conditions that permit to reach the goal: an input memory
state to cover the goal instruction can so be found by constraint solving. The tool currently deals with
arithmetic operations on integers, heap manipulation and conditional instructions. The implementation
of a strategy to avoid enumerating the paths that lead to the goal until finding an executable one
is in progress. Current work also includes dealing with polymorphic function calls.
PathCrawler is a tool prototype developed by the LSL laboratory of CEA
List. PathCrawler automatically generates test-case inputs guaranteeing
full structural coverage of the C function under test: all feasible
paths, all reachable branches, all k-paths,... PathCrawler runs an
automatically-instrumented version of the function under test on each
test-case as soon as it is generated in order to recover the path
covered by this test-case and ensure that the next test-case covers a
path which is not covered yet. Test-case generation is implemented using
constraint logic programming. To ensure that PathCrawler can be used on
real-life programs, current work focusses on the treatment of called
functions, the treatment of the precondition on the effective input
parameters under which the function is to be tested, the treatment of
pointer casts, the treatment of integer overflows and floating-point
numbers and the early detection of infeasible path prefixes.
