-
Reachability Analysis of Term Rewriting Systems with Timbuk
We present Timbuk - a tree automata library - which implements usual operation- s on tree automata as well as a completion algorithm used to compute an... -
Rewriting for Cryptographic Protocol Verification - Extended Version -
On a case study, we present a new approach for verifying cryptographic protocols, based on rewriting and on tree automata techniques. Protocols are operationally... -
Decidable Approximations of Sets of Descendants and Sets of Normal Forms - ex...
We present here decidable approximations of sets of descendants and sets of normal forms of Term Rewriting Systems, based on specific tree automata techniques. In the... -
Tracing the Origins of Verification Conditions
The typical program verification system is a batch tool that accepts as input a program annotated with Floyd-Hoare assertions, performs syntactic and semantic analysis... -
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.
