scientific article; zbMATH DE number 1953274
From MaRDI portal
Publication:4414726
zbMATH Open1026.68514MaRDI QIDQ4414726FDOQ4414726
Authors: Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jerome Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, Xavier Rival 
Publication date: 27 July 2003
Full work available at URL: http://link.springer.de/link/service/series/0558/bibs/2566/25660085.htm
Title of this publication is not available (Why is that?)
Recommendations
Cited In (73)
- Static blame for gradual typing
- Title not available (Why is that?)
- The Undefined Domain: Precise Relational Information for Entities That Do Not Exist
- Proving the Correctness of the Implementation of a Control-Command Algorithm
- Sweeping in Abstract Interpretation
- Learning a Strategy for Choosing Widening Thresholds from a Large Codebase
- Relational abstract interpretation of arrays in assembly code
- Clustered relational thread-modular abstract interpretation with local traces
- MDPs as distribution transformers: affine invariant synthesis for safety objectives
- Class invariants as abstract interpretation of trace semantics
- Sound non-statistical clustering of static analysis alarms
- Inferring Loop Invariants Using Postconditions
- Constructive Galois connections
- Incrementally closing octagons
- Generic abstraction of dictionaries and arrays
- A formally verified floating-point implementation of the compact position reporting algorithm
- Programming Languages and Systems
- Precise thread-modular abstract interpretation of concurrent programs using relational interference abstractions
- Static timing analysis -- what is special?
- A sparse evaluation technique for detailed semantic analyses
- Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol
- A minimalistic look at widening operators
- Improving the results of program analysis by abstract interpretation beyond the decreasing sequence
- A two-phase approach for conditional floating-point verification
- Deductive verification of floating-point Java programs in KeY
- Pentagons: a weakly relational abstract domain for the efficient validation of array accesses
- Termination of floating-point computations
- Stratified static analysis based on variable dependencies
- The abstract domain of trapezoid step functions
- Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness
- Acceleration of the abstract fixpoint computation in numerical program analysis
- An extension of lazy abstraction with interpolation for programs with arrays
- Unbounded-time analysis of guarded LTI systems with inputs by abstract acceleration
- Applications of polyhedral computations to the analysis and verification of hardware and software systems
- Temporal property verification as a program analysis task
- Widening and narrowing operators for abstract interpretation
- Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration
- Template polyhedra and bilinear optimization
- A divide-and-conquer approach for analysing overlaid data structures
- Static analysis of embedded real-time concurrent software with dynamic priorities
- Static analysis of binary code with memory indirections using polyhedra
- Compact Difference Bound Matrices
- Static analysis of run-time errors in embedded critical parallel C programs
- Implementing and reasoning about hash-consed data structures in Coq
- Demand-driven interprocedural analysis for map-based abstract domains
- Static contract checking with abstract interpretation
- Automation of quantitative information-flow analysis
- ASTREE
- Inferring functional properties of matrix manipulating programs by abstract interpretation
- Learning analysis strategies for Octagon and context sensitivity from labeled data generated by static analyses
- Title not available (Why is that?)
- Programming Languages and Systems
- The two variable per inequality abstract domain
- Integration of verification methods for program systems
- Mutation-Based Test Case Generation for Simulink Models
- The octagon abstract domain
- Analyzing Array Manipulating Programs by Program Transformation
- Combining model checking and data-flow analysis
- Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants
- Why does Astrée scale up?
- Abstract fixpoint computations with numerical acceleration methods
- Relational abstract domain of weighted hexagons
- Some ways to reduce the space dimension in polyhedra computations
- Improving strategies via SMT solving
- Sawja: static analysis workshop for Java
- Inferring complete initialization of arrays
- Generalizing the template polyhedral domain
- Integrated and automated abstract interpretation, verification and testing of C/C++ modules
- A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis
- An array content static analysis based on non-contiguous partitions
- Access-based localization for octagons
- Comparison of combinatorial signatures of global network dynamics generated by two classes of ODE models
- Abstract Interpretation of the Physical Inputs of Embedded Programs
Uses Software
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4414726)
