Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software
From MaRDI portal
Recommendations
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
This page was built for publication: Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4414726)
