Difference between revisions of "2012-01-28 Verification day"
(+Goran) |
(program) |
||
| Line 1: | Line 1: | ||
==Program== | ==Program== | ||
===Julien Henry: Big steps for static analysis=== | ===Julien Henry: Big steps for static analysis=== | ||
| + | 9h15-10h | ||
Static analysis by abstract interpretation traditionally follows the control-flow graph of the programs, with one inductive invariant being computed for every control node, computed by forward (or backward) propagation along control edges. One weakness of such an approach is that it enforces that the invariants at all nodes belong to the set of abstractions chosen; for instance, if one uses convex polyhedra, it enforces that all invariants are convex, thus conditions such as |x|≥1 cannot be represented, which may lead to imprecision and spurious warnings. | Static analysis by abstract interpretation traditionally follows the control-flow graph of the programs, with one inductive invariant being computed for every control node, computed by forward (or backward) propagation along control edges. One weakness of such an approach is that it enforces that the invariants at all nodes belong to the set of abstractions chosen; for instance, if one uses convex polyhedra, it enforces that all invariants are convex, thus conditions such as |x|≥1 cannot be represented, which may lead to imprecision and spurious warnings. | ||
We instead take big steps in the control graph, using SMT-solving to enumerate paths as needed (an explicit enumeration would lead to exponential blowup). | We instead take big steps in the control graph, using SMT-solving to enumerate paths as needed (an explicit enumeration would lead to exponential blowup). | ||
| Line 8: | Line 9: | ||
===David Monniaux: Path-focusing and policy iteration=== | ===David Monniaux: Path-focusing and policy iteration=== | ||
| − | + | 10h15-10h50h | |
Policy iteration is a method for computing strongest invariants for certain transition relations (e.g. disjunctions/conjunctions/projections in linear real algebra) in certain abstract domains (e.g. products of intervals, more generally template polyhedra). | Policy iteration is a method for computing strongest invariants for certain transition relations (e.g. disjunctions/conjunctions/projections in linear real algebra) in certain abstract domains (e.g. products of intervals, more generally template polyhedra). | ||
Policy iteration was initially formulated with one invariant per control point, but we adapted it to path-focusing, and even to a combination of predicate abstraction with polyhedral analysis. | Policy iteration was initially formulated with one invariant per control point, but we adapted it to path-focusing, and even to a combination of predicate abstraction with polyhedral analysis. | ||
| Line 15: | Line 16: | ||
===David Monniaux: Quick presentation of the VERASCO and STATOR projects=== | ===David Monniaux: Quick presentation of the VERASCO and STATOR projects=== | ||
| + | 10h50-11h | ||
* [http://verasco.imag.fr/ VERASCO: proved static analyzers] (ANR) | * [http://verasco.imag.fr/ VERASCO: proved static analyzers] (ANR) | ||
* [http://stator.imag.fr/ STATOR: advanced static analysis techniques] (ERC) | * [http://stator.imag.fr/ STATOR: advanced static analysis techniques] (ERC) | ||
===Goran Frehse: Calcul "lazy" avec des ensembles convexes représentés par des fonctions de support=== | ===Goran Frehse: Calcul "lazy" avec des ensembles convexes représentés par des fonctions de support=== | ||
| + | 11h05-11h50 | ||
===Thao Dang: Reachability analysis for polynomial dynamical systems using the Bernstein expansion=== | ===Thao Dang: Reachability analysis for polynomial dynamical systems using the Bernstein expansion=== | ||
| + | 13h-13h45 | ||
This paper is concerned with the reachability computation problem for polynomial discrete-time dynamical systems. Such computations constitute a crucial component in algorithmic verification tools for hybrid systems and embedded software with polynomial dynamics, which have found applications in many engineering domains. We describe two methods for over-approximating the reachable sets of such systems; these methods are based on a combination of the Bernstein expansion of polynomial functions and a representation of reachable sets by template polyhedra. Using a prototype implementation, the performance of the methods was demonstrated on a number of examples of control systems and biological systems. | This paper is concerned with the reachability computation problem for polynomial discrete-time dynamical systems. Such computations constitute a crucial component in algorithmic verification tools for hybrid systems and embedded software with polynomial dynamics, which have found applications in many engineering domains. We describe two methods for over-approximating the reachable sets of such systems; these methods are based on a combination of the Bernstein expansion of polynomial functions and a representation of reachable sets by template polyhedra. Using a prototype implementation, the performance of the methods was demonstrated on a number of examples of control systems and biological systems. | ||
===Marie-Laure Potet: Les besoins pour l'analyse de vulnérabilités=== | ===Marie-Laure Potet: Les besoins pour l'analyse de vulnérabilités=== | ||
| + | 13h50-14h30 | ||
(20 minutes) | (20 minutes) | ||
| Line 33: | Line 38: | ||
===Laurent Mounier: Analyse de teinte sur du code binaire=== | ===Laurent Mounier: Analyse de teinte sur du code binaire=== | ||
| + | 14h30-15h | ||
(~ 20 minutes) | (~ 20 minutes) | ||
| Line 39: | Line 45: | ||
===Radu Iosif: Acceleration Techniques for Program Verification=== | ===Radu Iosif: Acceleration Techniques for Program Verification=== | ||
| + | 15h05-16h50 | ||
By acceleration we understand the class of techniques based on a precise computation of the transitive closure of (a part of) the transition relation of the program. In the first part of this talk we show how acceleration can be combined with interpolation to generate inductive interpolants which are crucial in abstraction refinement. This combined method applies to sequential non-recursive programs. In the second part of this talk, we show how acceleration can be applied, in a modular fashion, to recursive program schemes. The result is a Newtonian underapproximation sequence that converges to the tuple of summary relations of all procedures in the program. We also define a class of programs for which our method is shown to be complete i.e. terminate with the precise result. | By acceleration we understand the class of techniques based on a precise computation of the transitive closure of (a part of) the transition relation of the program. In the first part of this talk we show how acceleration can be combined with interpolation to generate inductive interpolants which are crucial in abstraction refinement. This combined method applies to sequential non-recursive programs. In the second part of this talk, we show how acceleration can be applied, in a modular fashion, to recursive program schemes. The result is a Newtonian underapproximation sequence that converges to the tuple of summary relations of all procedures in the program. We also define a class of programs for which our method is shown to be complete i.e. terminate with the precise result. | ||
| Line 44: | Line 51: | ||
===Nicolas Peltier: On an abductive approach to error detection=== | ===Nicolas Peltier: On an abductive approach to error detection=== | ||
| + | 17h-17h45 | ||
Joint work: Thierry Boy de la Tour, Mnacho Echenim, Nicolas Peltier et Sophie Tourret | Joint work: Thierry Boy de la Tour, Mnacho Echenim, Nicolas Peltier et Sophie Tourret | ||
The development of efficient decision procedures for (combinations of) theories that are used in hardware and software verification has made it easier to guarantee the correctness of the systems under scrutiny. In addition to being as efficient as possible, many state-of-the-art SMT solvers now enjoy automated model building features that can be used to construct counter-examples of faulty systems, with the aim of helping the system designers detect and correct the erros it contains. However, analyzing these counter-examples can be a long and difficult task, and pinpointing the errors in the system can still require a lot of work. | The development of efficient decision procedures for (combinations of) theories that are used in hardware and software verification has made it easier to guarantee the correctness of the systems under scrutiny. In addition to being as efficient as possible, many state-of-the-art SMT solvers now enjoy automated model building features that can be used to construct counter-examples of faulty systems, with the aim of helping the system designers detect and correct the erros it contains. However, analyzing these counter-examples can be a long and difficult task, and pinpointing the errors in the system can still require a lot of work. | ||
| − | We propose to investigate what is, to the best of our knowledge, a new approach to the detection of bugs in a system. The idea behind this approach is that, rather than analyzing one or all the counter-examples of a formula, more valuable information can be inferred from the properties that hold in all the counter-examples of the formula. These properties can be generated using techniques from automated abductive reasoning, and we present here a few directions of research that are currently under investigation | + | We propose to investigate what is, to the best of our knowledge, a new approach to the detection of bugs in a system. The idea behind this approach is that, rather than analyzing one or all the counter-examples of a formula, more valuable information can be inferred from the properties that hold in all the counter-examples of the formula. These properties can be generated using techniques from automated abductive reasoning, and we present here a few directions of research that are currently under investigation. |
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
Revision as of 11:05, 24 January 2013
Contents
- 1 Program
- 1.1 Julien Henry: Big steps for static analysis
- 1.2 David Monniaux: Path-focusing and policy iteration
- 1.3 David Monniaux: Quick presentation of the VERASCO and STATOR projects
- 1.4 Goran Frehse: Calcul "lazy" avec des ensembles convexes représentés par des fonctions de support
- 1.5 Thao Dang: Reachability analysis for polynomial dynamical systems using the Bernstein expansion
- 1.6 Marie-Laure Potet: Les besoins pour l'analyse de vulnérabilités
- 1.7 Laurent Mounier: Analyse de teinte sur du code binaire
- 1.8 Radu Iosif: Acceleration Techniques for Program Verification
- 1.9 Nicolas Peltier: On an abductive approach to error detection
Program
Julien Henry: Big steps for static analysis
9h15-10h Static analysis by abstract interpretation traditionally follows the control-flow graph of the programs, with one inductive invariant being computed for every control node, computed by forward (or backward) propagation along control edges. One weakness of such an approach is that it enforces that the invariants at all nodes belong to the set of abstractions chosen; for instance, if one uses convex polyhedra, it enforces that all invariants are convex, thus conditions such as |x|≥1 cannot be represented, which may lead to imprecision and spurious warnings. We instead take big steps in the control graph, using SMT-solving to enumerate paths as needed (an explicit enumeration would lead to exponential blowup). We propose, in addition to the basic path-focused analysis some variant iteration scheme based on guided static analysis, and another for disjunctive invariants.
Joint work with Laure Gonnord, David Monniaux and Matthieu Moy.
David Monniaux: Path-focusing and policy iteration
10h15-10h50h Policy iteration is a method for computing strongest invariants for certain transition relations (e.g. disjunctions/conjunctions/projections in linear real algebra) in certain abstract domains (e.g. products of intervals, more generally template polyhedra). Policy iteration was initially formulated with one invariant per control point, but we adapted it to path-focusing, and even to a combination of predicate abstraction with polyhedral analysis.
Joint work with Thomas Gawlitza and Peter Schrammel.
David Monniaux: Quick presentation of the VERASCO and STATOR projects
10h50-11h
Goran Frehse: Calcul "lazy" avec des ensembles convexes représentés par des fonctions de support
11h05-11h50
Thao Dang: Reachability analysis for polynomial dynamical systems using the Bernstein expansion
13h-13h45
This paper is concerned with the reachability computation problem for polynomial discrete-time dynamical systems. Such computations constitute a crucial component in algorithmic verification tools for hybrid systems and embedded software with polynomial dynamics, which have found applications in many engineering domains. We describe two methods for over-approximating the reachable sets of such systems; these methods are based on a combination of the Bernstein expansion of polynomial functions and a representation of reachable sets by template polyhedra. Using a prototype implementation, the performance of the methods was demonstrated on a number of examples of control systems and biological systems.
Marie-Laure Potet: Les besoins pour l'analyse de vulnérabilités
13h50-14h30 (20 minutes)
Nous présentons nos travaux en cours dans le cadre de l'analyse de code vulnérable, en insistant notamment sur :
- les particularités de ce type d'analyse : code binaire, modèle mémoire ad hoc
- les conséquences sur les techniques d'analyse à utiliser ou développer
Laurent Mounier: Analyse de teinte sur du code binaire
14h30-15h (~ 20 minutes)
Nous présentons un exemple concret d'analyse développée pour la recherche de vulnérabilités : l'analyse de teinte.
Radu Iosif: Acceleration Techniques for Program Verification
15h05-16h50 By acceleration we understand the class of techniques based on a precise computation of the transitive closure of (a part of) the transition relation of the program. In the first part of this talk we show how acceleration can be combined with interpolation to generate inductive interpolants which are crucial in abstraction refinement. This combined method applies to sequential non-recursive programs. In the second part of this talk, we show how acceleration can be applied, in a modular fashion, to recursive program schemes. The result is a Newtonian underapproximation sequence that converges to the tuple of summary relations of all procedures in the program. We also define a class of programs for which our method is shown to be complete i.e. terminate with the precise result.
Joint work with EPFL (Lausanne), IMDEA (Madrid), FIT BUT (Brno)
Nicolas Peltier: On an abductive approach to error detection
17h-17h45
Joint work: Thierry Boy de la Tour, Mnacho Echenim, Nicolas Peltier et Sophie Tourret
The development of efficient decision procedures for (combinations of) theories that are used in hardware and software verification has made it easier to guarantee the correctness of the systems under scrutiny. In addition to being as efficient as possible, many state-of-the-art SMT solvers now enjoy automated model building features that can be used to construct counter-examples of faulty systems, with the aim of helping the system designers detect and correct the erros it contains. However, analyzing these counter-examples can be a long and difficult task, and pinpointing the errors in the system can still require a lot of work. We propose to investigate what is, to the best of our knowledge, a new approach to the detection of bugs in a system. The idea behind this approach is that, rather than analyzing one or all the counter-examples of a formula, more valuable information can be inferred from the properties that hold in all the counter-examples of the formula. These properties can be generated using techniques from automated abductive reasoning, and we present here a few directions of research that are currently under investigation.
