-
Proceedings 18th International Workshop on Logical and Semantic Frameworks, with Applications and 10th Workshop on Horn Clauses for Verification and Synthesis
Authors:
Temur Kutsia,
Daniel Ventura,
David Monniaux,
José F. Morales
Abstract:
This volume contains
* The post-proceedings of the Eighteenth Logical and Semantic Frameworks with Applications (LSFA 2023). The meeting was held on July 1-2, 2023, organised by the Sapienza Università di Roma, Italy. LSFA aims to bring researchers and students interested in theoretical and practical aspects of logical and semantic frameworks and their applications. The covered topics include pr…
▽ More
This volume contains
* The post-proceedings of the Eighteenth Logical and Semantic Frameworks with Applications (LSFA 2023). The meeting was held on July 1-2, 2023, organised by the Sapienza Università di Roma, Italy. LSFA aims to bring researchers and students interested in theoretical and practical aspects of logical and semantic frameworks and their applications. The covered topics include proof theory, type theory and rewriting theory, specification and deduction languages, and formal semantics of languages and systems.
* The post-proceedings of the Tenth Workshop on Horn clauses for Verification and Synthesis (HCVS 2023). The meeting was held on April 23, 2023 at the Institut Henri Poincaré in Paris. HCVS aims to bring together researchers working in the two communities of constraint/ logic programming (e.g., ICLP and CP), program verification (e.g., CAV, TACAS, and VMCAI), and automated deduction (e.g., CADE, IJCAR), on the topics of Horn clause based analysis, verification, and synthesis.
△ Less
Submitted 21 April, 2024;
originally announced April 2024.
-
Memory Simulations, Security and Optimization in a Verified Compiler
Authors:
David Monniaux
Abstract:
Current compilers implement security features and optimizations that require nontrivial semantic reasoning about pointers and memory allocation: the program after the insertion of the security feature, or after applying the optimization, must simulate the original program despite a different memory layout. In this article, we illustrate such reasoning on pointer allocations through memory extensi…
▽ More
Current compilers implement security features and optimizations that require nontrivial semantic reasoning about pointers and memory allocation: the program after the insertion of the security feature, or after applying the optimization, must simulate the original program despite a different memory layout. In this article, we illustrate such reasoning on pointer allocations through memory extensions and injections, as well as fine points on undefined values, by explaining how we implemented and proved correct two security features (stack canaries and pointer authentication) and one optimization (tail recursion elimination) in the CompCert formally verified compiler.
△ Less
Submitted 13 December, 2023;
originally announced December 2023.
-
Completeness in static analysis by abstract interpretation, a personal point of view
Authors:
David Monniaux
Abstract:
Static analysis by abstract interpretation is generally designed to be ''sound'', that is, it should not claim to establish properties that do not hold-in other words, not provide ''false negatives'' about possible bugs. A rarer requirement is that it should be ''complete'', meaning that it should be able to infer certain properties if they hold. This paper describes a number of practical issues a…
▽ More
Static analysis by abstract interpretation is generally designed to be ''sound'', that is, it should not claim to establish properties that do not hold-in other words, not provide ''false negatives'' about possible bugs. A rarer requirement is that it should be ''complete'', meaning that it should be able to infer certain properties if they hold. This paper describes a number of practical issues and questions related to completeness that I have come across over the years.
△ Less
Submitted 25 May, 2023; v1 submitted 17 November, 2022;
originally announced November 2022.
-
BAXMC: a CEGAR approach to Max#SAT
Authors:
Thomas Vigouroux,
Cristian Ene,
David Monniaux,
Laurent Mounier,
Marie-Laure Potet
Abstract:
Max#SAT is an important problem with multiple applications in security and program synthesis that is proven hard to solve. It is defined as: given a parameterized quantifier-free propositional formula compute parameters such that the number of models of the formula is maximal. As an extension, the formula can include an existential prefix. We propose a CEGAR-based algorithm and refinements thereof…
▽ More
Max#SAT is an important problem with multiple applications in security and program synthesis that is proven hard to solve. It is defined as: given a parameterized quantifier-free propositional formula compute parameters such that the number of models of the formula is maximal. As an extension, the formula can include an existential prefix. We propose a CEGAR-based algorithm and refinements thereof, based on either exact or approximate model counting, and prove its correctness in both cases. Our experiments show that this algorithm has much better effective complexity than the state of the art.
△ Less
Submitted 6 February, 2023; v1 submitted 2 November, 2022;
originally announced November 2022.
-
Formally verified 32- and 64-bit integer division using double-precision floating-point arithmetic
Authors:
David Monniaux,
Alice Pain
Abstract:
Some recent processors are not equipped with an integer division unit. Compilers then implement division by a call to a special function supplied by the processor designers, which implements division by a loop producing one bit of quotient per iteration. This hinders compiler optimizations and results in non-constant time computation, which is a problem in some applications. We advocate instead…
▽ More
Some recent processors are not equipped with an integer division unit. Compilers then implement division by a call to a special function supplied by the processor designers, which implements division by a loop producing one bit of quotient per iteration. This hinders compiler optimizations and results in non-constant time computation, which is a problem in some applications. We advocate instead using the processor's floating-point unit, and propose code that the compiler can easily interleave with other computations. We fully proved the correctness of our algorithm, which mixes floating-point and fixed-bitwidth integer computations, using the Coq proof assistant and successfully integrated it into the CompCert formally verified compiler.
△ Less
Submitted 18 July, 2022;
originally announced July 2022.
-
NP$^{\#P}$ = $\exists$PP and other remarks about maximized counting
Authors:
David Monniaux
Abstract:
We consider the following decision problem DMAX#SAT, and generalizations thereof: given a quantifier-free propositional formula $F(\mathbf{x},\mathbf{y})$, where $\mathbf{x},\mathbf{y}$ are tuples of variables, and a bound $B$, determine if there is $\vec{x}$ such that $\#\{\mathbf{y} \mid F(\mathbf{x},\mathbf{y})\} \geq B$. This is the decision version of the problem of MAX#SAT: finding…
▽ More
We consider the following decision problem DMAX#SAT, and generalizations thereof: given a quantifier-free propositional formula $F(\mathbf{x},\mathbf{y})$, where $\mathbf{x},\mathbf{y}$ are tuples of variables, and a bound $B$, determine if there is $\vec{x}$ such that $\#\{\mathbf{y} \mid F(\mathbf{x},\mathbf{y})\} \geq B$. This is the decision version of the problem of MAX#SAT: finding $\mathbf{x}$ and $B$ for maximal $B$.
△ Less
Submitted 24 February, 2022;
originally announced February 2022.
-
The complexity gap in the static analysis of cache accesses grows if procedure calls are added
Authors:
David Monniaux
Abstract:
The static analysis of cache accesses consists in correctly predicting which accesses are hits or misses. While there exist good exact and approximate analyses for caches implementing the least recently used (LRU) replacement policy, such analyses were harder to find for other replacement policies. A theoretical explanation was found: for an appropriate setting of analysis over control-flow graphs…
▽ More
The static analysis of cache accesses consists in correctly predicting which accesses are hits or misses. While there exist good exact and approximate analyses for caches implementing the least recently used (LRU) replacement policy, such analyses were harder to find for other replacement policies. A theoretical explanation was found: for an appropriate setting of analysis over control-flow graphs, cache analysis is PSPACE-complete for all common replacement policies (FIFO, PLRU, NMRU) except for LRU, for which it is only NP-complete. In this paper, we show that if procedure calls are added to the control flow, then the gap widens: analysis remains NP-complete for LRU, but becomes EXPTIME-complete for the three other policies. For this, we improve on earlier results on the complexity of reachability problems on Boolean programs with procedure calls. In addition, for the LRU policy we derive a backtracking algorithm as well as an approach for using it as a last resort after other analyses have failed to conclude.
△ Less
Submitted 31 January, 2022;
originally announced January 2022.
-
The Trusted Computing Base of the CompCert Verified Compiler
Authors:
David Monniaux,
Sylvain Boulmé
Abstract:
CompCert is the first realistic formally verified compiler: it provides a machine-checked mathematical proof that the code it generates matches the source code. Yet, there could be loopholes in this approach. We comprehensively analyze aspects of CompCert where errors could lead to incorrect code being generated. Possible issues range from the modeling of the source and the target languages to som…
▽ More
CompCert is the first realistic formally verified compiler: it provides a machine-checked mathematical proof that the code it generates matches the source code. Yet, there could be loopholes in this approach. We comprehensively analyze aspects of CompCert where errors could lead to incorrect code being generated. Possible issues range from the modeling of the source and the target languages to some techniques used to call external algorithms from within the compiler.
△ Less
Submitted 10 October, 2022; v1 submitted 25 January, 2022;
originally announced January 2022.
-
Simple, Light, Yet Formally Verified, Global Common Subexpression Elimination and Loop-Invariant Code Motion
Authors:
David Monniaux,
Cyril Six
Abstract:
We present an approach for implementing a formally certified loop-invariant code motion optimization by composing an unrolling pass and a formally certified yet efficient global subexpression elimination.This approach is lightweight: each pass comes with a simple and independent proof of correctness.Experiments show the approach significantly narrows the performance gap between the CompCert certif…
▽ More
We present an approach for implementing a formally certified loop-invariant code motion optimization by composing an unrolling pass and a formally certified yet efficient global subexpression elimination.This approach is lightweight: each pass comes with a simple and independent proof of correctness.Experiments show the approach significantly narrows the performance gap between the CompCert certified compiler and state-of-the-art optimizing compilers.Our static analysis employs an efficient yet verified hashed set structure, resulting in fast compilation.
△ Less
Submitted 4 May, 2021;
originally announced May 2021.
-
A task-based approach to parallel parametric linear programming solving, and application to polyhedral computations
Authors:
Camille Coti,
David Monniaux,
Hang Yu
Abstract:
Parametric linear programming is a central operation for polyhedral computations, as well as in certain control applications.Here we propose a task-based scheme for parallelizing it, with quasi-linear speedup over large problems.This type of parallel applications is challenging, because several tasks mightbe computing the same region. In this paper, we are presenting thealgorithm itself with a par…
▽ More
Parametric linear programming is a central operation for polyhedral computations, as well as in certain control applications.Here we propose a task-based scheme for parallelizing it, with quasi-linear speedup over large problems.This type of parallel applications is challenging, because several tasks mightbe computing the same region. In this paper, we are presenting thealgorithm itself with a parallel redundancy elimination algorithm, andconducting a thorough performance analysis.
△ Less
Submitted 29 September, 2020;
originally announced September 2020.
-
An Efficient Parametric Linear Programming Solver and Application to Polyhedral Projection
Authors:
Hang Yu,
David Monniaux
Abstract:
Polyhedral projection is a main operation of the polyhedron abstract domain.It can be computed via parametric linear programming (PLP), which is more efficient than the classic Fourier-Motzkin elimination method.In prior work, PLP was done in arbitrary precision rational arithmetic.In this paper, we present an approach where most of the computation is performed in floating-point arithmetic, then e…
▽ More
Polyhedral projection is a main operation of the polyhedron abstract domain.It can be computed via parametric linear programming (PLP), which is more efficient than the classic Fourier-Motzkin elimination method.In prior work, PLP was done in arbitrary precision rational arithmetic.In this paper, we present an approach where most of the computation is performed in floating-point arithmetic, then exact rational results are reconstructed.We also propose a workaround for a difficulty that plagued previous attempts at using PLP for computations on polyhedra: in general the linear programming problems are degenerate, resulting in redundant computations and geometric descriptions.
△ Less
Submitted 18 November, 2019;
originally announced November 2019.
-
Parallel parametric linear programming solving, and application to polyhedral computations
Authors:
Camille Coti,
David Monniaux,
Hang Yu
Abstract:
Parametric linear programming is central in polyhedral computations and in certain control applications.We propose a task-based scheme for parallelizing it, with quasi-linear speedup over large problems.
Parametric linear programming is central in polyhedral computations and in certain control applications.We propose a task-based scheme for parallelizing it, with quasi-linear speedup over large problems.
△ Less
Submitted 12 April, 2019;
originally announced April 2019.
-
On the complexity of cache analysis for different replacement policies
Authors:
David Monniaux,
Valentin Touzeau
Abstract:
Modern processors use cache memory: a memory access that "hits" the cache returns early, while a "miss" takes more time. Given a memory access in a program, cache analysis consists in deciding whether this access is always a hit, always a miss, or is a hit or a miss depending on execution. Such an analysis is of high importance for bounding the worst-case execution time of safety-critical real-tim…
▽ More
Modern processors use cache memory: a memory access that "hits" the cache returns early, while a "miss" takes more time. Given a memory access in a program, cache analysis consists in deciding whether this access is always a hit, always a miss, or is a hit or a miss depending on execution. Such an analysis is of high importance for bounding the worst-case execution time of safety-critical real-time programs.There exist multiple possible policies for evicting old data from the cache when new data are brought in, and different policies, though apparently similar in goals and performance, may be very different from the analysis point of view. In this paper, we explore these differences from a complexity-theoretical point of view. Specifically, we show that, among the common replacement policies, LRU (Least Recently Used) is the only one whose analysis is NP-complete, whereas the analysis problems for the other policies are PSPACE-complete.
△ Less
Submitted 23 September, 2019; v1 submitted 5 November, 2018;
originally announced November 2018.
-
Fast and exact analysis for LRU caches
Authors:
Claire Maïza,
Valentin Touzeau,
David Monniaux,
Jan Reineke
Abstract:
For applications in worst-case execution time analysis and in security, it is desirable to statically classify memory accesses into those that result in cache hits, and those that result in cache misses. Among cache replacement policies, the least recently used (LRU) policy has been studied the most and is considered to be the most predictable. The state-of-the-art in LRU cache analysis presents a…
▽ More
For applications in worst-case execution time analysis and in security, it is desirable to statically classify memory accesses into those that result in cache hits, and those that result in cache misses. Among cache replacement policies, the least recently used (LRU) policy has been studied the most and is considered to be the most predictable. The state-of-the-art in LRU cache analysis presents a tradeoff between precision and analysis efficiency: The classical approach to analyzing programs running on LRU caches, an abstract interpretation based on a range abstraction, is very fast but can be imprecise. An exact analysis was recently presented, but, as a last resort, it calls a model checker, which is expensive. In this paper, we develop an analysis based on abstract interpretation that comes close to the efficiency of the classical approach, while achieving exact classification of all memory accesses as the model-checking approach. Compared with the model-checking approach we observe speedups of several orders of magnitude. As a secondary contribution we show that LRU cache analysis problems are in general NP-complete.
△ Less
Submitted 20 December, 2018; v1 submitted 5 November, 2018;
originally announced November 2018.
-
Ascertaining Uncertainty for Efficient Exact Cache Analysis
Authors:
Valentin Touzeau,
Claire Maïza,
David Monniaux,
Jan Reineke
Abstract:
Static cache analysis characterizes a program's cache behavior by determining in a sound but approximate manner which memory accesses result in cache hits and which result in cache misses. Such information is valuable in optimizing compilers, worst-case execution time analysis, and side-channel attack quantification and mitigation.Cache analysis is usually performed as a combination of `must' and…
▽ More
Static cache analysis characterizes a program's cache behavior by determining in a sound but approximate manner which memory accesses result in cache hits and which result in cache misses. Such information is valuable in optimizing compilers, worst-case execution time analysis, and side-channel attack quantification and mitigation.Cache analysis is usually performed as a combination of `must' and `may' abstract interpretations, classifying instructions as either `always hit', `always miss', or `unknown'. Instructions classified as `unknown' might result in a hit or a miss depending on program inputs or the initial cache state. It is equally possible that they do in fact always hit or always miss, but the cache analysis is too coarse to see it.Our approach to eliminate this uncertainty consists in (i) a novel abstract interpretation able to ascertain that a particular instruction may definitely cause a hit and a miss on different paths, and (ii) an exact analysis, removing all remaining uncertainty, based on model checking, using abstract-interpretation results to prune down the model for scalability.We evaluated our approach on a variety of examples; it notably improves precision upon classical abstract interpretation at reasonable cost.
△ Less
Submitted 20 December, 2018; v1 submitted 28 September, 2017;
originally announced September 2017.
-
On the decidability of the existence of polyhedral invariants in transition systems
Authors:
David Monniaux
Abstract:
Automated program verification often proceeds by exhibiting inductive invariants entailing the desired properties.For numerical properties, a classical class of invariants is convex polyhedra: solution sets of system of linear (in)equalities.Forty years of research on convex polyhedral invariants have focused, on the one hand, on identifying "easier" subclasses, on the other hand on heuristics for…
▽ More
Automated program verification often proceeds by exhibiting inductive invariants entailing the desired properties.For numerical properties, a classical class of invariants is convex polyhedra: solution sets of system of linear (in)equalities.Forty years of research on convex polyhedral invariants have focused, on the one hand, on identifying "easier" subclasses, on the other hand on heuristics for finding general convex polyhedra.These heuristics are however not guaranteed to find polyhedral inductive invariants when they exist.To our best knowledge, the existence of polyhedral inductive invariants has never been proved to be undecidable.In this article, we show that the existence of convex polyhedral invariants is undecidable, even if there is only one control state in addition to the "bad" one.The question is still open if one is not allowed any nonlinear constraint.
△ Less
Submitted 15 May, 2018; v1 submitted 13 September, 2017;
originally announced September 2017.
-
Combining Forward and Backward Abstract Interpretation of Horn Clauses
Authors:
Alexey Bakhirkin,
David Monniaux
Abstract:
Alternation of forward and backward analyses is a standard technique in abstract interpretation of programs, which is in particular useful when we wish to prove unreachability of some undesired program states. The current state-of-the-art technique for combining forward (bottom-up, in logic programming terms) and backward (top-down) abstract interpretation of Horn clauses is query-answer transform…
▽ More
Alternation of forward and backward analyses is a standard technique in abstract interpretation of programs, which is in particular useful when we wish to prove unreachability of some undesired program states. The current state-of-the-art technique for combining forward (bottom-up, in logic programming terms) and backward (top-down) abstract interpretation of Horn clauses is query-answer transformation. It transforms a system of Horn clauses, such that standard forward analysis can propagate constraints both forward, and backward from a goal. Query-answer transformation is effective, but has issues that we wish to address. For that, we introduce a new backward collecting semantics, which is suitable for alternating forward and backward abstract interpretation of Horn clauses. We show how the alternation can be used to prove unreachability of the goal and how every subsequent run of an analysis yields a refined model of the system. Experimentally, we observe that combining forward and backward analyses is important for analysing systems that encode questions about reachability in C programs. In particular, the combination that follows our new semantics improves the precision of our own abstract interpreter, including when compared to a forward analysis of a query-answer-transformed system.
△ Less
Submitted 7 August, 2017; v1 submitted 5 July, 2017;
originally announced July 2017.
-
Model Checking of Cache for WCET Analysis Refinement
Authors:
Valentin Touzeau,
Claire Maïza,
David Monniaux
Abstract:
On real-time systems running under timing constraints, scheduling can be performed when one is aware of the worst case execution time (WCET) of tasks. Usually, the WCET of a task is unknown and schedulers make use of safe over-approximations given by static WCET analysis. To reduce the over-approximation, WCET analysis has to gain information about the underlying hardware behavior, such as pipelin…
▽ More
On real-time systems running under timing constraints, scheduling can be performed when one is aware of the worst case execution time (WCET) of tasks. Usually, the WCET of a task is unknown and schedulers make use of safe over-approximations given by static WCET analysis. To reduce the over-approximation, WCET analysis has to gain information about the underlying hardware behavior, such as pipelines and caches. In this paper, we focus on the cache analysis, which classifies memory accesses as hits/misses according to the set of possible cache states. We propose to refine the results of classical cache analysis using a model checker, introducing a new cache model for the least recently used (LRU) policy.
△ Less
Submitted 6 July, 2017; v1 submitted 27 January, 2017;
originally announced January 2017.
-
Formula Slicing: Inductive Invariants from Preconditions
Authors:
Egor George Karpenkov,
David Monniaux
Abstract:
We propose a "formula slicing" method for finding inductive invariants. It is based on the observation that many loops in the program affect only a small part of the memory, and many invariants which were valid before a loop are still valid after.
Given a precondition of the loop, obtained from the preceding program fragment, we weaken it until it becomes inductive. The weakening procedure is gu…
▽ More
We propose a "formula slicing" method for finding inductive invariants. It is based on the observation that many loops in the program affect only a small part of the memory, and many invariants which were valid before a loop are still valid after.
Given a precondition of the loop, obtained from the preceding program fragment, we weaken it until it becomes inductive. The weakening procedure is guided by counterexamples-to-induction given by an SMT solver. Our algorithm applies to programs with arbitrary loop structure, and it computes the strongest invariant in an abstract domain of weakenings of preconditions. We call this algorithm "formula slicing", as it effectively performs "slicing" on formulas derived from symbolic execution.
We evaluate our algorithm on the device driver benchmarks from the International Competition on Software Verification (SV-COMP), and we show that it is competitive with the state-of-the-art verification techniques.
△ Less
Submitted 2 October, 2016; v1 submitted 29 September, 2016;
originally announced September 2016.
-
A Survey of Satisfiability Modulo Theory
Authors:
David Monniaux
Abstract:
Satisfiability modulo theory (SMT) consists in testing the satisfiability of first-order formulas over linear integer or real arithmetic, or other theories. In this survey, we explain the combination of propositional satisfiability and decision procedures for conjunctions known as DPLL(T), and the alternative "natural domain" approaches. We also cover quantifiers, Craig interpolants, polynomial ar…
▽ More
Satisfiability modulo theory (SMT) consists in testing the satisfiability of first-order formulas over linear integer or real arithmetic, or other theories. In this survey, we explain the combination of propositional satisfiability and decision procedures for conjunctions known as DPLL(T), and the alternative "natural domain" approaches. We also cover quantifiers, Craig interpolants, polynomial arithmetic, and how SMT solvers are used in automated software analysis.
△ Less
Submitted 15 June, 2016;
originally announced June 2016.
-
An encoding of array verification problems into array-free Horn clauses
Authors:
David Monniaux,
Laure Gonnord
Abstract:
Automatically verifying safety properties of programs is hard, and it is even harder if the program acts upon arrays or other forms of maps. Many approaches exist for verifying programs operating upon Boolean and integer values (e.g. abstract interpretation, counterexample-guided abstraction refinement using interpolants), but transposing them to array properties has been fraught with difficulties…
▽ More
Automatically verifying safety properties of programs is hard, and it is even harder if the program acts upon arrays or other forms of maps. Many approaches exist for verifying programs operating upon Boolean and integer values (e.g. abstract interpretation, counterexample-guided abstraction refinement using interpolants), but transposing them to array properties has been fraught with difficulties.In contrast to most preceding approaches, we do not introduce a new abstract domain or a new interpolation procedure for arrays. Instead, we generate an abstraction as a scalar problem and feed it to a preexisting solver, with tunable precision.Our transformed problem is expressed using Horn clauses, a common format with clear and unambiguous logical semantics for verification problems. An important characteristic of our encoding is that it creates a nonlinear Horn problem, with tree unfoldings, even though following "flatly" the control-graph structure ordinarily yields a linear Horn problem, with linear unfoldings. That is, our encoding cannot be expressed by an encoding into another control-flow graph problem, and truly leverages the capacity of the Horn clause format.We illustrate our approach with a completely automated proof of the functional correctness of selection sort.
△ Less
Submitted 30 September, 2015;
originally announced September 2015.
-
Program Analysis with Local Policy Iteration
Authors:
George Karpenkov,
David Monniaux,
Philipp Wendler
Abstract:
We present a new algorithm for deriving numerical invariants that combines the precision of max-policy iteration with the flexibility and scalability of conventional Kleene iterations. It is defined in the Configurable Program Analysis (CPA) framework, thus allowing inter-analysis communication.
It uses adjustable-block encoding in order to traverse loop-free program sections, possibly containin…
▽ More
We present a new algorithm for deriving numerical invariants that combines the precision of max-policy iteration with the flexibility and scalability of conventional Kleene iterations. It is defined in the Configurable Program Analysis (CPA) framework, thus allowing inter-analysis communication.
It uses adjustable-block encoding in order to traverse loop-free program sections, possibly containing branching, without introducing extra abstraction. Our technique operates over any template linear constraint domain, including the interval and octagon domains; templates can also be derived from the program source.
The implementation is evaluated on a set of benchmarks from the Software Verification Competition (SV-Comp). It competes favorably with state-of-the-art analyzers.
△ Less
Submitted 3 November, 2015; v1 submitted 11 September, 2015;
originally announced September 2015.
-
A simple abstraction of arrays and maps by program translation
Authors:
David Monniaux,
Francesco Alberti
Abstract:
We present an approach for the static analysis of programs handling arrays, with a Galois connection between the semantics of the array program and semantics of purely scalar operations. The simplest way to implement it is by automatic, syntactic transformation of the array program into a scalar program followed analysis of the scalar program with any static analysis technique (abstract interpreta…
▽ More
We present an approach for the static analysis of programs handling arrays, with a Galois connection between the semantics of the array program and semantics of purely scalar operations. The simplest way to implement it is by automatic, syntactic transformation of the array program into a scalar program followed analysis of the scalar program with any static analysis technique (abstract interpretation, acceleration, predicate abstraction,.. .). The scalars invariants thus obtained are translated back onto the original program as universally quantified array invariants. We illustrate our approach on a variety of examples, leading to the " Dutch flag " algorithm.
△ Less
Submitted 12 June, 2015;
originally announced June 2015.
-
How to Compute Worst-Case Execution Time by Optimization Modulo Theory and a Clever Encoding of Program Semantics
Authors:
Julien Henry,
Mihail Asavoae,
David Monniaux,
Claire Maïza
Abstract:
In systems with hard real-time constraints, it is necessary to compute upper bounds on the worst-case execution time (WCET) of programs; the closer the bound to the real WCET, the better. This is especially the case of synchronous reactive control loops with a fixed clock; the WCET of the loop body must not exceed the clock period. We compute the WCET (or at least a close upper bound thereof) as t…
▽ More
In systems with hard real-time constraints, it is necessary to compute upper bounds on the worst-case execution time (WCET) of programs; the closer the bound to the real WCET, the better. This is especially the case of synchronous reactive control loops with a fixed clock; the WCET of the loop body must not exceed the clock period. We compute the WCET (or at least a close upper bound thereof) as the solution of an optimization modulo theory problem that takes into account the semantics of the program, in contrast to other methods that compute the longest path whether or not it is feasible according to these semantics. Optimization modulo theory extends satisfiability modulo theory (SMT) to maximization problems. Immediate encodings of WCET problems into SMT yield formulas intractable for all current production-grade solvers; this is inherent to the DPLL(T) approach to SMT implemented in these solvers. By conjoining some appropriate "cuts" to these formulas, we considerably reduce the computation time of the SMT-solver. We experimented our approach on a variety of control programs, using the OTAWA analyzer both as baseline and as underlying microarchitectural analysis for our analysis, and show notable improvement on the WCET bound on a variety of benchmarks and control programs.
△ Less
Submitted 30 May, 2014;
originally announced May 2014.
-
Speeding Up Logico-Numerical Strategy Iteration (extended version)
Authors:
David Monniaux,
Peter Schrammel
Abstract:
We introduce an efficient combination of polyhedral analysis and predicate partitioning. Template polyhedral analysis abstracts numerical variables inside a program by one polyhedron per control location, with a priori fixed directions for the faces. The strongest inductive invariant in such an abstract domain may be computed by upward strategy iteration. If the transition relation includes disjun…
▽ More
We introduce an efficient combination of polyhedral analysis and predicate partitioning. Template polyhedral analysis abstracts numerical variables inside a program by one polyhedron per control location, with a priori fixed directions for the faces. The strongest inductive invariant in such an abstract domain may be computed by upward strategy iteration. If the transition relation includes disjunctions and existential quantifiers (a succinct representation for an exponential set of paths), this invariant can be computed by a combination of strategy iteration and satisfiability modulo theory (SMT) solving. Unfortunately, the above approaches lead to unacceptable space and time costs if applied to a program whose control states have been partitioned according to predicates. We therefore propose a modification of the strategy iteration algorithm where the strategies are stored succinctly, and the linear programs to be solved at each iteration step are simplified according to an equivalence relation. We have implemented the technique in a prototype tool and we demonstrate on a series of examples that the approach performs significantly better than previous strategy iteration techniques.
△ Less
Submitted 2 October, 2014; v1 submitted 10 March, 2014;
originally announced March 2014.
-
Implementing and reasoning about hash-consed data structures in Coq
Authors:
Thomas Braibant,
Jacques-Henri Jourdan,
David Monniaux
Abstract:
We report on four different approaches to implementing hash-consing in Coq programs. The use cases include execution inside Coq, or execution of the extracted OCaml code. We explore the different trade-offs between faithful use of pristine extracted code, and code that is fine-tuned to make use of OCaml programming constructs not available in Coq. We discuss the possible consequences in terms of p…
▽ More
We report on four different approaches to implementing hash-consing in Coq programs. The use cases include execution inside Coq, or execution of the extracted OCaml code. We explore the different trade-offs between faithful use of pristine extracted code, and code that is fine-tuned to make use of OCaml programming constructs not available in Coq. We discuss the possible consequences in terms of performances and guarantees. We use the running example of binary decision diagrams and then demonstrate the generality of our solutions by applying them to other examples of hash-consed data structures.
△ Less
Submitted 25 September, 2015; v1 submitted 7 November, 2013;
originally announced November 2013.
-
Implementing hash-consed structures in Coq
Authors:
Thomas Braibant,
Jacques-Henri Jourdan,
David Monniaux
Abstract:
We report on three different approaches to use hash-consing in programs certified with the Coq system, using binary decision diagrams (BDD) as running example. The use cases include execution inside Coq, or execution of the extracted OCaml code. There are different trade-offs between faithful use of pristine extracted code, and code that is fine-tuned to make use of OCaml programming constructs no…
▽ More
We report on three different approaches to use hash-consing in programs certified with the Coq system, using binary decision diagrams (BDD) as running example. The use cases include execution inside Coq, or execution of the extracted OCaml code. There are different trade-offs between faithful use of pristine extracted code, and code that is fine-tuned to make use of OCaml programming constructs not available in Coq. We discuss the possible consequences in terms of performances and guarantees.
△ Less
Submitted 22 April, 2013;
originally announced April 2013.
-
Efficient Generation of Correctness Certificates for the Abstract Domain of Polyhedra
Authors:
Alexis Fouilhé,
David Monniaux,
Michaël Périn
Abstract:
Polyhedra form an established abstract domain for inferring runtime properties of programs using abstract interpretation. Computations on them need to be certified for the whole static analysis results to be trusted. In this work, we look at how far we can get down the road of a posteriori verification to lower the overhead of certification of the abstract domain of polyhedra. We demonstrate metho…
▽ More
Polyhedra form an established abstract domain for inferring runtime properties of programs using abstract interpretation. Computations on them need to be certified for the whole static analysis results to be trusted. In this work, we look at how far we can get down the road of a posteriori verification to lower the overhead of certification of the abstract domain of polyhedra. We demonstrate methods for making the cost of inclusion certificate generation negligible. From a performance point of view, our single-representation, constraints-based implementation compares with state-of-the-art implementations.
△ Less
Submitted 3 April, 2013;
originally announced April 2013.
-
Invariant Generation through Strategy Iteration in Succinctly Represented Control Flow Graphs
Authors:
Thomas Martin Gawlitza,
David Monniaux
Abstract:
We consider the problem of computing numerical invariants of programs, for instance bounds on the values of numerical program variables. More specifically, we study the problem of performing static analysis by abstract interpretation using template linear constraint domains. Such invariants can be obtained by Kleene iterations that are, in order to guarantee termination, accelerated by widening o…
▽ More
We consider the problem of computing numerical invariants of programs, for instance bounds on the values of numerical program variables. More specifically, we study the problem of performing static analysis by abstract interpretation using template linear constraint domains. Such invariants can be obtained by Kleene iterations that are, in order to guarantee termination, accelerated by widening operators. In many cases, however, applying this form of extrapolation leads to invariants that are weaker than the strongest inductive invariant that can be expressed within the abstract domain in use. Another well-known source of imprecision of traditional abstract interpretation techniques stems from their use of join operators at merge nodes in the control flow graph. The mentioned weaknesses may prevent these methods from proving safety properties. The technique we develop in this article addresses both of these issues: contrary to Kleene iterations accelerated by widening operators, it is guaranteed to yield the strongest inductive invariant that can be expressed within the template linear constraint domain in use. It also eschews join operators by distinguishing all paths of loop-free code segments. Formally speaking, our technique computes the least fixpoint within a given template linear constraint domain of a transition relation that is succinctly expressed as an existentially quantified linear real arithmetic formula. In contrast to previously published techniques that rely on quantifier elimination, our algorithm is proved to have optimal complexity: we prove that the decision problem associated with our fixpoint problem is in the second level of the polynomial-time hierarchy.
△ Less
Submitted 28 September, 2012; v1 submitted 4 September, 2012;
originally announced September 2012.
-
PAGAI: a path sensitive static analyzer
Authors:
Julien Henry,
David Monniaux,
Matthieu Moy
Abstract:
We describe the design and the implementation of PAGAI, a new static analyzer working over the LLVM compiler infrastructure, which computes inductive invariants on the numerical variables of the analyzed program. PAGAI implements various state-of-the-art algorithms combining abstract interpretation and decision procedures (SMT-solving), focusing on distinction of paths inside the control flow grap…
▽ More
We describe the design and the implementation of PAGAI, a new static analyzer working over the LLVM compiler infrastructure, which computes inductive invariants on the numerical variables of the analyzed program. PAGAI implements various state-of-the-art algorithms combining abstract interpretation and decision procedures (SMT-solving), focusing on distinction of paths inside the control flow graph while avoiding systematic exponential enumerations. It is parametric in the abstract domain in use, the iteration algorithm, and the decision procedure. We compared the time and precision of various combinations of analysis algorithms and abstract domains, with extensive experiments both on personal benchmarks and widely available GNU programs.
△ Less
Submitted 17 July, 2012;
originally announced July 2012.
-
Succinct Representations for Abstract Interpretation
Authors:
Julien Henry,
David Monniaux,
Matthieu Moy
Abstract:
Abstract interpretation techniques can be made more precise by distinguishing paths inside loops, at the expense of possibly exponential complexity. SMT-solving techniques and sparse representations of paths and sets of paths avoid this pitfall. We improve previously proposed techniques for guided static analysis and the generation of disjunctive invariants by combining them with techniques for su…
▽ More
Abstract interpretation techniques can be made more precise by distinguishing paths inside loops, at the expense of possibly exponential complexity. SMT-solving techniques and sparse representations of paths and sets of paths avoid this pitfall. We improve previously proposed techniques for guided static analysis and the generation of disjunctive invariants by combining them with techniques for succinct representations of paths and symbolic representations for transitions based on static single assignment. Because of the non-monotonicity of the results of abstract interpretation with widening operators, it is difficult to conclude that some abstraction is more precise than another based on theoretical local precision results. We thus conducted extensive comparisons between our new techniques and previous ones, on a variety of open-source packages.
△ Less
Submitted 19 June, 2012;
originally announced June 2012.
-
Stratified Static Analysis Based on Variable Dependencies
Authors:
David Monniaux,
Julien Le Guen
Abstract:
In static analysis by abstract interpretation, one often uses widening operators in order to enforce convergence within finite time to an inductive invariant. Certain widening operators, including the classical one over finite polyhedra, exhibit an unintuitive behavior: analyzing the program over a subset of its variables may lead a more precise result than analyzing the original program! In this…
▽ More
In static analysis by abstract interpretation, one often uses widening operators in order to enforce convergence within finite time to an inductive invariant. Certain widening operators, including the classical one over finite polyhedra, exhibit an unintuitive behavior: analyzing the program over a subset of its variables may lead a more precise result than analyzing the original program! In this article, we present simple workarounds for such behavior.
△ Less
Submitted 12 September, 2011;
originally announced September 2011.
-
Modular Abstractions of Reactive Nodes using Disjunctive Invariants
Authors:
David Monniaux,
Martin Bodin
Abstract:
We wish to abstract nodes in a reactive programming language, such as Lustre, into nodes with a simpler control structure, with a bound on the number of control states. In order to do so, we compute disjunctive invariants in predicate abstraction, with a bounded number of disjuncts, then we abstract the node, each disjunct representing an abstract state. The computation of the disjunctive invarian…
▽ More
We wish to abstract nodes in a reactive programming language, such as Lustre, into nodes with a simpler control structure, with a bound on the number of control states. In order to do so, we compute disjunctive invariants in predicate abstraction, with a bounded number of disjuncts, then we abstract the node, each disjunct representing an abstract state. The computation of the disjunctive invariant is performed by a form of quantifier elimination expressed using SMT-solving. The same method can also be used to obtain disjunctive loop invariants.
△ Less
Submitted 9 September, 2011;
originally announced September 2011.
-
Using Bounded Model Checking to Focus Fixpoint Iterations
Authors:
David Monniaux,
Laure Gonnord
Abstract:
Two classical sources of imprecision in static analysis by abstract interpretation are widening and merge operations. Merge operations can be done away by distinguishing paths, as in trace partitioning, at the expense of enumerating an exponential number of paths. In this article, we describe how to avoid such systematic exploration by focusing on a single path at a time, designated by SMT-solving…
▽ More
Two classical sources of imprecision in static analysis by abstract interpretation are widening and merge operations. Merge operations can be done away by distinguishing paths, as in trace partitioning, at the expense of enumerating an exponential number of paths. In this article, we describe how to avoid such systematic exploration by focusing on a single path at a time, designated by SMT-solving. Our method combines well with acceleration techniques, thus doing away with widenings as well in some cases. We illustrate it over the well-known domain of convex polyhedra.
△ Less
Submitted 14 June, 2011;
originally announced June 2011.
-
On the Generation of Positivstellensatz Witnesses in Degenerate Cases
Authors:
David Monniaux,
Pierre Corbineau
Abstract:
One can reduce the problem of proving that a polynomial is nonnegative, or more generally of proving that a system of polynomial inequalities has no solutions, to finding polynomials that are sums of squares of polynomials and satisfy some linear equality (Positivstellensatz). This produces a witness for the desired property, from which it is reasonably easy to obtain a formal proof of the propert…
▽ More
One can reduce the problem of proving that a polynomial is nonnegative, or more generally of proving that a system of polynomial inequalities has no solutions, to finding polynomials that are sums of squares of polynomials and satisfy some linear equality (Positivstellensatz). This produces a witness for the desired property, from which it is reasonably easy to obtain a formal proof of the property suitable for a proof assistant such as Coq. The problem of finding a witness reduces to a feasibility problem in semidefinite programming, for which there exist numerical solvers. Unfortunately, this problem is in general not strictly feasible, meaning the solution can be a convex set with empty interior, in which case the numerical optimization method fails. Previously published methods thus assumed strict feasibility; we propose a workaround for this difficulty. We implemented our method and illustrate its use with examples, including extractions of proofs to Coq.
△ Less
Submitted 23 May, 2011;
originally announced May 2011.
-
Improving Strategies via SMT Solving
Authors:
Thomas Martin Gawlitza,
David Monniaux
Abstract:
We consider the problem of computing numerical invariants of programs by abstract interpretation. Our method eschews two traditional sources of imprecision: (i) the use of widening operators for enforcing convergence within a finite number of iterations (ii) the use of merge operations (often, convex hulls) at the merge points of the control flow graph. It instead computes the least inductive inva…
▽ More
We consider the problem of computing numerical invariants of programs by abstract interpretation. Our method eschews two traditional sources of imprecision: (i) the use of widening operators for enforcing convergence within a finite number of iterations (ii) the use of merge operations (often, convex hulls) at the merge points of the control flow graph. It instead computes the least inductive invariant expressible in the domain at a restricted set of program points, and analyzes the rest of the code en bloc. We emphasize that we compute this inductive invariant precisely. For that we extend the strategy improvement algorithm of [Gawlitza and Seidl, 2007]. If we applied their method directly, we would have to solve an exponentially sized system of abstract semantic equations, resulting in memory exhaustion. Instead, we keep the system implicit and discover strategy improvements using SAT modulo real linear arithmetic (SMT). For evaluating strategies we use linear programming. Our algorithm has low polynomial space complexity and performs for contrived examples in the worst case exponentially many strategy improvement steps; this is unsurprising, since we show that the associated abstract reachability problem is Pi-p-2-complete.
△ Less
Submitted 14 January, 2011;
originally announced January 2011.
-
Automatic Modular Abstractions for Template Numerical Constraints
Authors:
David Monniaux
Abstract:
We propose a method for automatically generating abstract transformers for static analysis by abstract interpretation. The method focuses on linear constraints on programs operating on rational, real or floating-point variables and containing linear assignments and tests. Given the specification of an abstract domain, and a program block, our method automatically outputs an implementation of the c…
▽ More
We propose a method for automatically generating abstract transformers for static analysis by abstract interpretation. The method focuses on linear constraints on programs operating on rational, real or floating-point variables and containing linear assignments and tests. Given the specification of an abstract domain, and a program block, our method automatically outputs an implementation of the corresponding abstract transformer. It is thus a form of program transformation. In addition to loop-free code, the same method also applies for obtaining least fixed points as functions of the precondition, which permits the analysis of loops and recursive functions. The motivation of our work is data-flow synchronous programming languages, used for building control-command embedded systems, but it also applies to imperative and functional programming. Our algorithms are based on quantifier elimination and symbolic manipulation techniques over linear arithmetic formulas. We also give less general results for nonlinear constraints and nonlinear program constructs.
△ Less
Submitted 26 May, 2010;
originally announced May 2010.
-
Automatic modular abstractions for template numerical constraints
Authors:
David Monniaux
Abstract:
We propose a method for automatically generating abstract transformers for static analysis by abstract interpretation. The method focuses on linear constraints on programs operating on rational, real or floating-point variables and containing linear assignments and tests. In addition to loop-free code, the same method also applies for obtaining least fixed points as functions of the precondition,…
▽ More
We propose a method for automatically generating abstract transformers for static analysis by abstract interpretation. The method focuses on linear constraints on programs operating on rational, real or floating-point variables and containing linear assignments and tests. In addition to loop-free code, the same method also applies for obtaining least fixed points as functions of the precondition, which permits the analysis of loops and recursive functions. Our algorithms are based on new quantifier elimination and symbolic manipulation techniques. Given the specification of an abstract domain, and a program block, our method automatically outputs an implementation of the corresponding abstract transformer. It is thus a form of program transformation. The motivation of our work is data-flow synchronous programming languages, used for building control-command embedded systems, but it also applies to imperative and functional programming.
△ Less
Submitted 31 May, 2010; v1 submitted 22 September, 2009;
originally announced September 2009.
-
On using floating-point computations to help an exact linear arithmetic decision procedure
Authors:
David Monniaux
Abstract:
We consider the decision problem for quantifier-free formulas whose atoms are linear inequalities interpreted over the reals or rationals. This problem may be decided using satisfiability modulo theory (SMT), using a mixture of a SAT solver and a simplex-based decision procedure for conjunctions. State-of-the-art SMT solvers use simplex implementations over rational numbers, which perform well f…
▽ More
We consider the decision problem for quantifier-free formulas whose atoms are linear inequalities interpreted over the reals or rationals. This problem may be decided using satisfiability modulo theory (SMT), using a mixture of a SAT solver and a simplex-based decision procedure for conjunctions. State-of-the-art SMT solvers use simplex implementations over rational numbers, which perform well for typical problems arising from model-checking and program analysis (sparse inequalities, small coefficients) but are slow for other applications (denser problems, larger coefficients). We propose a simple preprocessing phase that can be adapted on existing SMT solvers and that may be optionally triggered. Despite using floating-point computations, our method is sound and complete - it merely affects efficiency. We implemented the method and provide benchmarks showing that this change brings a naive and slow decision procedure ("textbook simplex" with rational numbers) up to the efficiency of recent SMT solvers, over test cases arising from model-checking, and makes it definitely faster than state-of-the-art SMT solvers on dense examples.
△ Less
Submitted 22 April, 2009;
originally announced April 2009.
-
A minimalistic look at widening operators
Authors:
David Monniaux
Abstract:
We consider the problem of formalizing the familiar notion of widening in abstract interpretation in higher-order logic. It turns out that many axioms of widening (e.g. widening sequences are ascending) are not useful for proving correctness. After kee** only useful axioms, we give an equivalent characterization of widening as a lazily constructed well-founded tree. In type systems supporting…
▽ More
We consider the problem of formalizing the familiar notion of widening in abstract interpretation in higher-order logic. It turns out that many axioms of widening (e.g. widening sequences are ascending) are not useful for proving correctness. After kee** only useful axioms, we give an equivalent characterization of widening as a lazily constructed well-founded tree. In type systems supporting dependent products and sums, this tree can be made to reflect the condition of correct termination of the widening sequence.
△ Less
Submitted 23 November, 2009; v1 submitted 21 February, 2009;
originally announced February 2009.
-
Automatic Modular Abstractions for Linear Constraints
Authors:
David Monniaux
Abstract:
We propose a method for automatically generating abstract transformers for static analysis by abstract interpretation. The method focuses on linear constraints on programs operating on rational, real or floating-point variables and containing linear assignments and tests. In addition to loop-free code, the same method also applies for obtaining least fixed points as functions of the precondition…
▽ More
We propose a method for automatically generating abstract transformers for static analysis by abstract interpretation. The method focuses on linear constraints on programs operating on rational, real or floating-point variables and containing linear assignments and tests. In addition to loop-free code, the same method also applies for obtaining least fixed points as functions of the precondition, which permits the analysis of loops and recursive functions. Our algorithms are based on new quantifier elimination and symbolic manipulation techniques. Given the specification of an abstract domain, and a program block, our method automatically outputs an implementation of the corresponding abstract transformer. It is thus a form of program transformation. The motivation of our work is data-flow synchronous programming languages, used for building control-command embedded systems, but it also applies to imperative and functional programming.
△ Less
Submitted 2 November, 2008;
originally announced November 2008.
-
A Quantifier Elimination Algorithm for Linear Real Arithmetic
Authors:
David Monniaux
Abstract:
We propose a new quantifier elimination algorithm for the theory of linear real arithmetic. This algorithm uses as subroutine satisfiability modulo this theory, a problem for which there are several implementations available. The quantifier elimination algorithm presented in the paper is compared, on examples arising from program analysis problems, to several other implementations, all of which…
▽ More
We propose a new quantifier elimination algorithm for the theory of linear real arithmetic. This algorithm uses as subroutine satisfiability modulo this theory, a problem for which there are several implementations available. The quantifier elimination algorithm presented in the paper is compared, on examples arising from program analysis problems, to several other implementations, all of which cannot solve some of the examples that our algorithm solves easily.
△ Less
Submitted 4 September, 2008; v1 submitted 11 March, 2008;
originally announced March 2008.
-
Applying the Z-transform for the static analysis of floating-point numerical filters
Authors:
David Monniaux
Abstract:
Digital linear filters are used in a variety of applications (sound treatment, control/command, etc.), implemented in software, in hardware, or a combination thereof. For safety-critical applications, it is necessary to bound all variables and outputs of all filters. We give a compositional, effective abstraction for digital linear filters expressed as block diagrams, yielding sound, precise bou…
▽ More
Digital linear filters are used in a variety of applications (sound treatment, control/command, etc.), implemented in software, in hardware, or a combination thereof. For safety-critical applications, it is necessary to bound all variables and outputs of all filters. We give a compositional, effective abstraction for digital linear filters expressed as block diagrams, yielding sound, precise bounds for fixed-point or floating-point implementations of the filters.
△ Less
Submitted 2 June, 2007;
originally announced June 2007.
-
An Abstract Monte-Carlo Method for the Analysis of Probabilistic Programs
Authors:
David Monniaux
Abstract:
We introduce a new method, combination of random testing and abstract interpretation, for the analysis of programs featuring both probabilistic and non-probabilistic nondeterminism. After introducing "ordinary" testing, we show how to combine testing and abstract interpretation and give formulas linking the precision of the results to the number of iterations. We then discuss complexity and opti…
▽ More
We introduce a new method, combination of random testing and abstract interpretation, for the analysis of programs featuring both probabilistic and non-probabilistic nondeterminism. After introducing "ordinary" testing, we show how to combine testing and abstract interpretation and give formulas linking the precision of the results to the number of iterations. We then discuss complexity and optimization issues and end with some experimental results.
△ Less
Submitted 30 January, 2007;
originally announced January 2007.
-
A Static Analyzer for Large Safety-Critical Software
Authors:
Bruno Blanchet,
Patrick Cousot,
Radhia Cousot,
Jerôme Feret,
Laurent Mauborgne,
Antoine Miné,
David Monniaux,
Xavier Rival
Abstract:
We show that abstract interpretation-based static program analysis can be made efficient and precise enough to formally verify a class of properties for a family of large programs with few or no false alarms. This is achieved by refinement of a general purpose static analyzer and later adaptation to particular programs of the family by the end-user through parametrization. This is applied to the…
▽ More
We show that abstract interpretation-based static program analysis can be made efficient and precise enough to formally verify a class of properties for a family of large programs with few or no false alarms. This is achieved by refinement of a general purpose static analyzer and later adaptation to particular programs of the family by the end-user through parametrization. This is applied to the proof of soundness of data manipulation operations at the machine level for periodic synchronous safety critical embedded software. The main novelties are the design principle of static analyzers by refinement and adaptation through parametrization, the symbolic manipulation of expressions to improve the precision of abstract transfer functions, the octagon, ellipsoid, and decision tree abstract domains, all with sound handling of rounding errors in floating point computations, widening strategies (with thresholds, delayed) and the automatic determination of the parameters (parametrized packing).
△ Less
Submitted 30 January, 2007;
originally announced January 2007.
-
The pitfalls of verifying floating-point computations
Authors:
David Monniaux
Abstract:
Current critical systems commonly use a lot of floating-point computations, and thus the testing or static analysis of programs containing floating-point operators has become a priority. However, correctly defining the semantics of common implementations of floating-point is tricky, because semantics may change with many factors beyond source-code level, such as choices made by compilers. We her…
▽ More
Current critical systems commonly use a lot of floating-point computations, and thus the testing or static analysis of programs containing floating-point operators has become a priority. However, correctly defining the semantics of common implementations of floating-point is tricky, because semantics may change with many factors beyond source-code level, such as choices made by compilers. We here give concrete examples of problems that can appear and solutions to implement in analysis software.
△ Less
Submitted 22 May, 2008; v1 submitted 30 January, 2007;
originally announced January 2007.
-
The parallel implementation of the Astrée static analyzer
Authors:
David Monniaux
Abstract:
The Astrée static analyzer is a specialized tool that can prove the absence of runtime errors, including arithmetic overflows, in large critical programs. Kee** analysis times reasonable for industrial use is one of the design objectives. In this paper, we discuss the parallel implementation of the analysis.
The Astrée static analyzer is a specialized tool that can prove the absence of runtime errors, including arithmetic overflows, in large critical programs. Kee** analysis times reasonable for industrial use is one of the design objectives. In this paper, we discuss the parallel implementation of the analysis.
△ Less
Submitted 30 January, 2007;
originally announced January 2007.
