-
Abstracting Call-Stacks for Interprocedural Verification of Imperative Programs
We address in this paper the verification of imperative programs with recursion. Our approach consists in using abstract interpretation to relate the standard... -
PAGAI: a path sensitive static analyzer
International audience -
Proving Negative Conjectures on Equational Theories using Induction and Abstr...
In this paper we present a method to prove automatically initial negative properties on equational specifications. This method tends to combine induction and abstract... -
Intraprocedural Pointer Analysis for Container-Centric Applications
As programmers look forward to designing high performance applications with object-oriented models, compilers must support higher-level analyses and optimizations.... -
Static Analysis of Java for Distributed and Parallel Programming
We investigate the use of static analysis for building distributed and parallel programs in Java. We first quickly explain a principle of seamless sequential,... -
When the Decreasing Sequence Fails
International audience -
Extending Abstract Acceleration Methods to Data-Flow Programs with Numerical ...
International audience -
Logico-Numerical Abstract Acceleration and Application to the Verification of...
International audience -
Applying abstract acceleration to (co-)reachability analysis of reactive prog...
International audience -
Logico-Numerical Abstract Acceleration and Application to the Verification of...
Acceleration methods are commonly used for speeding up the convergence of loops in reachability analysis of counter machine models. Applying these methods to... -
Logico-Numerical Max-Strategy Iteration
International audience -
Proving termination by policy iteration
International audience -
Control-flow analysis of function calls and returns by abstract interpretation
International audience -
McScM: A General Framework for the Verification of Communicating Machines
International audience -
Knockout Prediction for Reaction Networks with Partial Kinetic Information
International audience -
Sardana: an Automatic Tool for Numerical Accuracy Optimization
International audience -
A New Abstract Domain for the Representation of Mathematically Equivalent Exp...
International audience -
Synthesis of Arithmetic Expressions for the Fixed-Point Arithmetic: The Sarda...
International audience -
Abstract Interpretation of FIFO channels
We address the analysis and the verification of communicating systems, which are systems built from sequential processes communicating via unbounded FIFO channels. We...
