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)

• 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
• Combining Model Checking and Data-Flow Analysis
• A Hybrid Denotational Semantics for Hybrid Systems
• TreeKs: A Functor to Make Numerical Abstract Domains Scalable
• The Reduced Product of Abstract Domains and the Combination of Decision Procedures
• Sawja: Static Analysis Workshop for Java
• 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
• 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
• Generalizing the Template Polyhedral Domain
• Structural Abstract Interpretation: A Formal Study Using Coq
• 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
• Building Certified Static Analysers by Modular Construction of Well-founded Lattices
• 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
• An Abstract Interpretation Framework for the Round-Off Error Analysis of Floating-Point Programs
• 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
• Precise Thread-Modular Abstract Interpretation of Concurrent Programs Using Relational Interference Abstractions
• 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
• Taming the Wrapping of Integer Arithmetic
• Demand-driven interprocedural analysis for map-based abstract domains
• Experimental evaluation of numerical domains for inferring ranges
• Tools and Algorithms for the Construction and Analysis of Systems
• A galois connection calculus for abstract interpretation
• 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.
• A parametric segmentation functor for fully automatic and scalable array content analysis
• 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
• Constructive Galois Connections
• Comparison of Combinatorial Signatures of Global Network Dynamics Generated by Two Classes of ODE Models
• 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
• Static Analysis of Run-Time Errors in Embedded Critical Parallel C Programs
• Static Analysis of String Manipulations in Critical Embedded C Programs
• Static Contract Checking with Abstract Interpretation
• Abstract fixpoint computations with numerical acceleration methods
• Relational abstract domain of weighted hexagons
• Some ways to reduce the space dimension in polyhedra computations
• Inferring complete initialization of arrays
• A Data Driven Approach for Algebraic Loop Invariants
• Stratified Static Analysis Based on Variable Dependencies
• Invariant Generation through Strategy Iteration in Succinctly Represented Control Flow Graphs
• 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
• Automatic modular abstractions for linear constraints
• Static Analysis
• A framework for verification and debugging of resource usage properties: resource usage verification
• An Accurate Join for Zonotopes, Preserving Affine Input/Output Relations
• Loop invariants
• ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs
• Precondition Inference from Intermittent Assertions and Application to Contracts on Collections
• Incrementally closing octagons
• Formal analysis of the compact position reporting algorithm
• Improving Strategies via SMT Solving
• Programming Languages and Systems
• Automation of Quantitative Information-Flow Analysis
• On the efficiency of convex polyhedra
• Automatic Modular Abstractions for Template Numerical Constraints
• Sound Non-statistical Clustering of Static Analysis Alarms
• Hardware-Dependent Proofs of Numerical Programs
• Proving the Correctness of the Implementation of a Control-Command Algorithm
• Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration
• Programming Languages and Systems
• Verified compilation of floating-point computations
• Compact Difference Bound Matrices
• Converting One Type-Based Abstract Domain to Another
• Integrated and Automated Abstract Interpretation, Verification and Testing of C/C++ Modules
• Static analysis of run-time errors in embedded real-time parallel C programs
• Access-Based Localization for Octagons
• 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

This page was built for software: ASTREE