ASTREE

swMATH13704MaRDI QIDQ25618FDOQ25618

Author name not available (Why is that?)

Described by source

• Programming Languages and Systems
• Why does Astrée scale up?
• Unnamed Publication

Cited In (only showing first 100 items - show all)

• An abstract interpretation framework for the round-off error analysis of floating-point programs
• Class invariants as abstract interpretation of trace semantics
• Inferring Loop Invariants Using Postconditions
• Efficient SAT-based bounded model checking for software verification
• Static Analysis in Disjunctive Numerical Domains
• A Hybrid Denotational Semantics for Hybrid Systems
• Constructive Galois connections
• Precise thread-modular abstract interpretation of concurrent programs using relational interference abstractions
• A generic framework for heap and value analyses of object-oriented programming languages
• An abstract domain to infer symbolic ranges over nonnegative parameters
• A data driven approach for algebraic loop invariants
• A minimalistic look at widening operators
• Improving the results of program analysis by abstract interpretation beyond the decreasing sequence
• Abstract Interpretation of Symbolic Execution with Explicit State Updates
• 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
• Structural Abstract Interpretation: A Formal Study Using Coq
• Stratified static analysis based on variable dependencies
• Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness
• Acceleration of the abstract fixpoint computation in numerical program analysis
• Discovering invariants via simple component analysis
• Proof-carrying code from certified abstract interpretation and fixpoint compression
• An extension of lazy abstraction with interpolation for programs with arrays
• Deciding floating-point logic with abstract conflict driven clause learning
• Weakening additivity in adjoining closures
• Verification, Model Checking, and Abstract Interpretation
• Applications of polyhedral computations to the analysis and verification of hardware and software systems
• Temporal property verification as a program analysis task
• Template polyhedra and bilinear optimization
• Splitting the Control Flow with Boolean Flags
• Convergence: integrating termination and abort-freedom
• A divide-and-conquer approach for analysing overlaid data structures
• Static analysis of embedded real-time concurrent software with dynamic priorities
• Polynomial function intervals for floating-point software verification
• Static analysis of run-time errors in embedded critical parallel C programs
• Taming the Wrapping of Integer Arithmetic
• \textsf{TreeKs}: a functor to make numerical abstract domains scalable
• Demand-driven interprocedural analysis for map-based abstract domains
• Static contract checking with abstract interpretation
• Experimental evaluation of numerical domains for inferring ranges
• Tools and Algorithms for the Construction and Analysis of Systems
• 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
• Programming languages and systems. 14th European symposium on programming, ESOP 2005, held as part of the joint European conferences on theory and practice of software, ETAPS 2005, Edinburgh, UK, April 4--8, 2005. Proceedings.
• Building certified static analysers by modular construction of well-founded lattices
• A parametric segmentation functor for fully automatic and scalable array content analysis
• Invariant generation through strategy iteration in succinctly represented control flow graphs
• Programming Languages and Systems
• Programming Languages and Systems
• Exploring approximations for floating-point arithmetic using UppSAT
• Checking array bounds by abstract interpretation and symbolic expressions
• The two variable per inequality abstract domain
• Integration of verification methods for program systems
• Wave equation numerical resolution: a comprehensive mechanized proof of a C program
• The octagon abstract domain
• Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic
• Combining model checking and data-flow analysis
• Static Analysis of String Manipulations in Critical Embedded C Programs
• Abstract fixpoint computations with numerical acceleration methods
• Relational abstract domain of weighted hexagons
• Some ways to reduce the space dimension in polyhedra computations
• A Galois connection calculus for abstract interpretation
• Sawja: static analysis workshop for Java
• The reduced product of abstract domains and the combination of decision procedures
• Inferring complete initialization of arrays
• Formal verification of numerical programs: from C annotated programs to mechanical proofs
• Theories, solvers and static analysis by abstract interpretation
• Programming languages and systems. Third Asian symposium, APLAS 2005, Tsukuba, Japan, November 2--5, 2005. Proceedings
• Generalizing the template polyhedral domain
• Automatic modular abstractions for linear constraints
• Static Analysis
• Comparison of combinatorial signatures of global network dynamics generated by two classes of ODE models
• A framework for verification and debugging of resource usage properties: resource usage verification
• Sound non-statistical clustering of static analysis alarms
• Incrementally closing octagons
• Generic abstraction of dictionaries and arrays
• Formal analysis of the compact position reporting algorithm
• Programming Languages and Systems
• On the efficiency of convex polyhedra
• Hardware-Dependent Proofs of Numerical Programs
• An accurate join for zonotopes, preserving affine input/output relations
• Proving the Correctness of the Implementation of a Control-Command Algorithm
• Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration
• Loop invariants: analysis, classification, and examples
• Programming Languages and Systems
• Verified compilation of floating-point computations
• A scalable segmented decision tree abstract domain
• Compact Difference Bound Matrices
• ConSORT: context- and flow-sensitive ownership refinement types for imperative programs
• Automation of quantitative information-flow analysis
• Converting One Type-Based Abstract Domain to Another
• Static analysis of run-time errors in embedded real-time parallel C programs
• An abstract memory functor for verified C static analyzers
• Mutation-Based Test Case Generation for Simulink Models
• An approximation framework for solvers and decision procedures
• FEVS: a functional equivalence verification suite for high-performance scientific computing
• Learning a Strategy for Choosing Widening Thresholds from a Large Codebase
• Abstract Interpretation of FIFO Replacement
• Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants
• Precondition inference from intermittent assertions and application to contracts on collections

This page was built for software: ASTREE