-
A Logic of Reachable Patterns in Linked Data-Structures
Original article available at http://www.sciencedirect.com. -
A library of Taylor models for PVS automatic proof checker
We present in this report a library to compute with Taylor models, a technique extending interval arithmetic to reduce decorrelation and to solve differential... -
Factorising temporal specifications
This paper proposes a method to factorise the verification of temporal properties for multi-threaded programs over groups of different threads. Essentially, the method... -
Specifying Imperative ML-Like Programs Using Dynamic Logic
International audience -
Synchronous composition of discretized control actions: design, verification ...
International audience -
Constraint solver over floating-point numbers designed for program verification
The verification of programs with floating-point numbers computation is an important issue in the development of critical software systems. Computations over... -
Decidable Approximations of Sets of Descendants and Sets of Normal forms
Colloque avec actes et comité de lecture.
