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

(77)

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

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)