scientific article; zbMATH DE number 1953274
From MaRDI portal
Publication:4414726
zbMath1026.68514MaRDI QIDQ4414726
Jerome Feret, Bruno Blanchet, Laurent Mauborgne, Patrick Cousot, Xavier Rival, David Monniaux, Antoine Miné, Radhia Cousot
Publication date: 27 July 2003
Full work available at URL: http://link.springer.de/link/service/series/0558/bibs/2566/25660085.htm
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items
Improving the results of program analysis by abstract interpretation beyond the decreasing sequence, Sound Non-statistical Clustering of Static Analysis Alarms, Combining Model Checking and Data-Flow Analysis, Compact Difference Bound Matrices, Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness, Why does Astrée scale up?, Learning a Strategy for Choosing Widening Thresholds from a Large Codebase, Automation of Quantitative Information-Flow Analysis, A minimalistic look at widening operators, Termination of floating-point computations, Some ways to reduce the space dimension in polyhedra computations, The octagon abstract domain, The Undefined Domain: Precise Relational Information for Entities That Do Not Exist, Inferring complete initialization of arrays, Analyzing Array Manipulating Programs by Program Transformation, Unbounded-Time Analysis of Guarded LTI Systems with Inputs by Abstract Acceleration, Relational abstract interpretation of arrays in assembly code, Precise Thread-Modular Abstract Interpretation of Concurrent Programs Using Relational Interference Abstractions, A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis, Acceleration of the abstract fixpoint computation in numerical program analysis, A divide-and-conquer approach for analysing overlaid data structures, Temporal property verification as a program analysis task, Comparison of Combinatorial Signatures of Global Network Dynamics Generated by Two Classes of ODE Models, The two variable per inequality abstract domain, An extension of lazy abstraction with interpolation for programs with arrays, Generalizing the Template Polyhedral Domain, Improving Strategies via SMT Solving, Static Analysis of Run-Time Errors in Embedded Critical Parallel C Programs, A two-phase approach for conditional floating-point verification, Deductive verification of floating-point Java programs in KeY, An array content static analysis based on non-contiguous partitions, The abstract domain of trapezoid step functions, Class invariants as abstract interpretation of trace semantics, Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants, Access-Based Localization for Octagons, Generic Abstraction of Dictionaries and Arrays, Sweeping in Abstract Interpretation, Stratified Static Analysis Based on Variable Dependencies, Inferring Loop Invariants Using Postconditions, Integrated and Automated Abstract Interpretation, Verification and Testing of C/C++ Modules, Widening and narrowing operators for abstract interpretation, A formally verified floating-point implementation of the compact position reporting algorithm, Pentagons: a weakly relational abstract domain for the efficient validation of array accesses, Demand-driven interprocedural analysis for map-based abstract domains, Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration, Learning analysis strategies for Octagon and context sensitivity from labeled data generated by static analyses, Inferring functional properties of matrix manipulating programs by abstract interpretation, Mutation-Based Test Case Generation for Simulink Models, Static Contract Checking with Abstract Interpretation, Sawja: Static Analysis Workshop for Java, Abstract Interpretation of the Physical Inputs of Embedded Programs, Abstract Fixpoint Computations with Numerical Acceleration Methods, Relational Abstract Domain of Weighted Hexagons, Constructive Galois Connections, ASTREE, Proving the Correctness of the Implementation of a Control-Command Algorithm, Applications of polyhedral computations to the analysis and verification of hardware and software systems, Template polyhedra and bilinear optimization, Integration of verification methods for program systems, Incrementally closing octagons, A sparse evaluation technique for detailed semantic analyses, Implementing and reasoning about hash-consed data structures in Coq
Uses Software
