ASTREE
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Access-based localization for octagons
- Comparison of combinatorial signatures of global network dynamics generated by two classes of ODE models
- Transfer function synthesis without quantifier elimination
- An abstract interpretation framework for the round-off error analysis of floating-point programs
- A framework for verification and debugging of resource usage properties: resource usage verification
- Class invariants as abstract interpretation of trace semantics
- Efficient SAT-based bounded model checking for software verification
- Sound non-statistical clustering of static analysis alarms
- Inferring Loop Invariants Using Postconditions
- Static Analysis in Disjunctive Numerical Domains
- Constructive Galois connections
- A Hybrid Denotational Semantics for Hybrid Systems
- Incrementally closing octagons
- Formal analysis of the compact position reporting algorithm
- Generic abstraction of dictionaries and arrays
- Precise thread-modular abstract interpretation of concurrent programs using relational interference abstractions
- Programming Languages and Systems
- A generic framework for heap and value analyses of object-oriented programming languages
- An abstract domain to infer symbolic ranges over nonnegative parameters
- A minimalistic look at widening operators
- Improving the results of program analysis by abstract interpretation beyond the decreasing sequence
- A data driven approach for algebraic loop invariants
- A novel analysis space for pointer analysis and its application for bug finding
- Pentagons: a weakly relational abstract domain for the efficient validation of array accesses
- Abstract Interpretation of Symbolic Execution with Explicit State Updates
- Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness
- Structural Abstract Interpretation: A Formal Study Using Coq
- Stratified static analysis based on variable dependencies
- On the efficiency of convex polyhedra
- Acceleration of the abstract fixpoint computation in numerical program analysis
- Discovering invariants via simple component analysis
- An extension of lazy abstraction with interpolation for programs with arrays
- Deciding floating-point logic with abstract conflict driven clause learning
- Proof-carrying code from certified abstract interpretation and fixpoint compression
- Weakening additivity in adjoining closures
- Applications of polyhedral computations to the analysis and verification of hardware and software systems
- Verification, Model Checking, and Abstract Interpretation
- Temporal property verification as a program analysis task
- Hardware-Dependent Proofs of Numerical Programs
- 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
- An accurate join for zonotopes, preserving affine input/output relations
- Splitting the Control Flow with Boolean Flags
- Verified compilation of floating-point computations
- Convergence: integrating termination and abort-freedom
- Loop invariants: analysis, classification, and examples
- Programming Languages and Systems
- Static analysis of embedded real-time concurrent software with dynamic priorities
- A scalable segmented decision tree abstract domain
- A divide-and-conquer approach for analysing overlaid data structures
- Polynomial function intervals for floating-point software verification
- Apron
- MPI-CHECK
- Sawja
- Cogent
- Zing
- DiVer
- TinyOS
- BLAST
- ACSL
- PHAVer
- Caduceus
- Gappa
- Aspic
- ISP
- Dagger
- PPL
- OCaml
- Goanna
- DART
- Cseq
- Predator
- JACK
- Gauss
- Consit
- PolyPaver
- SymmPa
- Lackwit
- Interproc
- MARMOT
- AutoMOTGen
- CBMC
- Soot
- julia
- InvGen
- Galculator
- YASM
- PolyLib
- Orion
- TVLA
- Threader
- SIMGRID
- RoVerGeNe
- NModel
- BAP
- MoonWalker
- SatAbs
- Traffic 4
- PAGAI
This page was built for software: ASTREE
