The Reduced Product of Abstract Domains and the Combination of Decision Procedures

No abstract is available for this paper.

• Publication year

  2011

• Venue

  Foundations of Software Science and Computation Structure

• Publication date

  2011-03-26

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1007/978-3-642-19805-2_31
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Logical Abstract Domains and Interpretations

  2010cited by this paper
• View-Augmented Abstractions

  2010cited by this paper
• A combination framework for tracking partition sizes

  2009cited by this paper
• Lifting abstract interpreters to quantified logical domains

  2008cited by this paper
• Safer unsafe code for .NET

  2008influential reference
• Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings

  2007cited by this paper
• Logical Interpretation: Static Program Analysis Using Theorem Proving

  2007cited by this paper
• The calculus of computation - decision procedures with applications to verification

  2007cited by this paper
• Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics

  2006cited by this paper
• Combining abstract interpreters

  2006cited by this paper
• Symbolic Implementation of the Best Transformer

  2004cited by this paper
• Path-Sensitive Analysis for Linear Arithmetic and Uninterpreted Functions

  2004cited by this paper
• Analysis of Recursive Game Graphs Using Data Flow Equations

  2004cited by this paper
• Unions of non-disjoint theories and combinations of satisfiability procedures

  2003cited by this paper
• Combining Non-Stably Infinite Theories

  2003cited by this paper
• Combining Shostak Theories

  2002cited by this paper
• Theorem Proving with Structured Theories

  2001cited by this paper
• A New Correctness Proof of the {Nelson-Oppen} Combination Procedure

  1996cited by this paper
• Improving the Results of Static Analyses Programs by Local Decreasing Iteration

  1992cited by this paper
• Simplification by Cooperating Decision Procedures

  1979influential reference
• Systematic design of program analysis frameworks

  1979cited by this paper
• Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints

  1977cited by this paper

• Abstract String Domain Defined with Word Equations as a Reduced Product (Extended Version)

  2025cites this paper
• Solvable Tuple Patterns and Their Applications to Program Verification

  2025cites this paper
• Strided Difference Bound Matrices

  2024cites this paper
• Automatic Inference of Relational Object Invariants

  2024cites this paper
• A Personal Historical Perspective on Abstract Interpretation

  2024cites this paper
• Precise Sparse Abstract Execution via Cross-Domain Interaction

  2024cites this paper
• Abstract Interpretation: From 0, 1, to ∞

  2023cites this paper
• Combining E-Graphs with Abstract Interpretation

  2022cites this paper
• A Sensible Approach to Speculative Automatic Parallelization

  2021cites this paper
• Automated policy synthesis for system call sandboxing

  2020cites this paper
• Verified Software. Theories, Tools, and Experiments: 11th International Conference, VSTTE 2019, New York City, NY, USA, July 13–14, 2019, Revised Selected Papers

  2020cites this paper
• SCAF: a speculation-aware collaborative dependence analysis framework

  2020cites this paper
• Verified from Scratch: Program Analysis for Learners' Programs

  2020cites this paper
• Formal Methods. FM 2019 International Workshops: Porto, Portugal, October 7–11, 2019, Revised Selected Papers, Part II

  2020cites this paper
• Combination of Boxes and Polyhedra Abstractions for Constraint Solving

  2019cites this paper
• Combinations of Reusable Abstract Domains for a Multilingual Static Analyzer

  2019cites this paper
• Automatic Inference of Hyperproperties

  2018cites this paper
• A collaborative dependence analysis framework

  2017cites this paper
• Block-Wise Abstract Interpretation by Combining Abstract Domains with SMT

  2017cites this paper
• Verasco: a Formally Verified C Static Analyzer

  2016cites this paper
• Rahft: A Tool for Verifying Horn Clauses Using Abstract Interpretation and Finite Tree Automata

  2016cites this paper
• Components for automatic horn clause verification

  2016cites this paper
• Formalizing Communication Between Numerical Abstract Domains ?

  2015cites this paper
• Adaptable Static Analysis of Executables for proving the Absence of Vulnerabilities

  2015cites this paper
• SMT-Based and Disjunctive Relational Abstract Domains for StaticAnalysis

  2015cites this paper
• Abstract satisfaction

  2014cites this paper
• Modularly Combining Numeric Abstract Domains with Points-to Analysis, and a Scalable Static Numeric Analyzer for Java

  2014cites this paper
• An Abstract Domain Combinator for Separately Conjoining Memory Abstractions

  2014cites this paper
• Abstract interpretation: past, present and future

  2014cites this paper
• Abstract conflict driven learning

  2013cites this paper
• Complete Instantiation-Based Interpolation

  2013cites this paper
• Separation Logic Modulo Theories

  2013cites this paper
• Incremental Invariant Generation Using Logic-Based Automatic Abstract Transformers

  2013cites this paper
• An Abstract Interpretation of DPLL(T)

  2013cites this paper
• NASA Formal Methods

  2013influential citation
• Deciding floating-point logic with abstract conflict driven clause learning

  2013cites this paper
• THÈSE Pour obtenir le grade de DOCTEUR DE L ’ UNIVERSITÉ DE GRENOBLE

  2013cites this paper
• An Abstract Domain for Bit-Vector Inequalities

  2013influential citation
• Automatic abstraction for bit-vectors using decision procedures

  2013cites this paper
• Invariant stream generators using automatic abstract transformers based on a decidable logic

  2012cites this paper
• Satisfiability Solvers Are Static Analysers

  2012cites this paper
• Deciding floating-point logic with systematic abstraction

  2012cites this paper
• Formal Verification by Abstract Interpretation

  2012cites this paper
• An abstract interpretation framework for refactoring with application to extract methods with contracts

  2012cites this paper
• Logico-Numerical Verification Methods for Discrete and Hybrid Systems

  2012cites this paper
• Static Analysis and Verification of Aerospace Software by Abstract Interpretation

  2010cites this paper