-
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... -
A PCC Architecture based on Certified Abstract Interpretation
Proof Carrying Code (PCC) is a technique for downloading mobile code on a host machine while ensuring that the code adheres to the host's security policy. We show how... -
Succinct Representations for Abstract Interpretation
International audience -
Abstract acceleration in Linear relation analysis
{Linear Relation Analysis~\cite{cousot78,halbwach79} is now a classical abstract interpretation based on an approximation of reachable numerical states of a program by...
