scientific article; zbMATH DE number 1953274

MaRDI QIDQ4414726zbMATH OpenFDO

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

Mathematics Subject Classification ID

Theory of software (68N99)

Recommendations

• Programming Languages and Systems
• Static timing analysis -- what is special?
• Programming Languages and Systems
• Correct Hardware Design and Verification Methods
• Static analysis of embedded real-time concurrent software with dynamic priorities

Cited in

(73)

• 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
• Class invariants as abstract interpretation of trace semantics
• Sound non-statistical clustering of static analysis alarms
• Inferring Loop Invariants Using Postconditions
• Constructive Galois connections
• Static blame for gradual typing
• Incrementally closing octagons
• A formally verified floating-point implementation of the compact position reporting algorithm
• Generic abstraction of dictionaries and arrays
• Precise thread-modular abstract interpretation of concurrent programs using relational interference abstractions
• Static timing analysis -- what is special?
• Programming Languages and Systems
• A sparse evaluation technique for detailed semantic analyses
• A minimalistic look at widening operators
• Improving the results of program analysis by abstract interpretation beyond the decreasing sequence
• Pentagons: a weakly relational abstract domain for the efficient validation of array accesses
• Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol
• A two-phase approach for conditional floating-point verification
• Deductive verification of floating-point Java programs in KeY
• Termination of floating-point computations
• The abstract domain of trapezoid step functions
• Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness
• Stratified static analysis based on variable dependencies
• Acceleration of the abstract fixpoint computation in numerical program analysis
• An extension of lazy abstraction with interpolation for programs with arrays
• scientific article; zbMATH DE number 2088933 (Why is no real title available?)
• The Undefined Domain: Precise Relational Information for Entities That Do Not Exist
• Applications of polyhedral computations to the analysis and verification of hardware and software systems
• Unbounded-time analysis of guarded LTI systems with inputs by abstract acceleration
• 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
• Proving the Correctness of the Implementation of a Control-Command Algorithm
• Template polyhedra and bilinear optimization
• Static analysis of embedded real-time concurrent software with dynamic priorities
• A divide-and-conquer approach for analysing overlaid data structures
• Static analysis of binary code with memory indirections using polyhedra
• ASTREE
• Compact Difference Bound Matrices
• Static analysis of run-time errors in embedded critical parallel C programs
• Demand-driven interprocedural analysis for map-based abstract domains
• Implementing and reasoning about hash-consed data structures in Coq
• Static contract checking with abstract interpretation
• Automation of quantitative information-flow analysis
• 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
• scientific article; zbMATH DE number 2080754 (Why is no real title available?)
• The two variable per inequality abstract domain
• Programming Languages and Systems
• Integration of verification methods for program systems
• Sweeping in Abstract Interpretation
• The octagon abstract domain
• Mutation-Based Test Case Generation for Simulink Models
• Learning a Strategy for Choosing Widening Thresholds from a Large Codebase
• 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?
• Some ways to reduce the space dimension in polyhedra computations
• Abstract fixpoint computations with numerical acceleration methods
• Relational abstract domain of weighted hexagons
• Relational abstract interpretation of arrays in assembly code
• Improving strategies via SMT solving
• Inferring complete initialization of arrays
• Sawja: static analysis workshop for Java
• Clustered relational thread-modular abstract interpretation with local traces
• MDPs as distribution transformers: affine invariant synthesis for safety objectives
• Generalizing the template polyhedral domain
• A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis
• Integrated and automated abstract interpretation, verification and testing of C/C++ modules
• An array content static analysis based on non-contiguous partitions

Describes a project that uses

Uses Software

• OCaml

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)