Parametric shape analysis via 3-valued logic

No abstract is available for this paper.

• Publication year

  1999

• Venue

  ACM-SIGACT Symposium on Principles of Programming Languages

• Publication date

  Unknown publication date

• Fields of study

  Mathematics, Computer Science

• Identifiers
  DOI 10.1145/292540.292552
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Verifying safety properties of concurrent Java programs using 3-valued logic

  2001cited by this paper
• Verifying safety properties of concurrent Java programs using 3-valued logic

  2001cited by this paper
• TVLA: A System for Implementing Static Analyses

  2000cited by this paper
• Putting static analysis to work for verification: A case study

  2000cited by this paper
• A Kleene Analysis of Mobile Ambients

  2000cited by this paper
• Compile-Time Debugging of C Programs Working on Trees

  2000cited by this paper
• Descriptive Complexity

  1999cited by this paper
• Experience with Predicate Abstraction

  1999cited by this paper
• A Decidable Logic for Describing Linked Data Structures

  1999cited by this paper
• Parametri Shape Analysis via 3-Valued Logi

  1999cited by this paper
• Mobile Ambients

  1998cited by this paper
• Arity Bounds in First-Order Incremental Evaluation and Definition of Polynomial Time Database Queries

  1998cited by this paper
• Dyn-FO: A Parallel, Dynamic Complexity Class

  1997cited by this paper
• Automatic verification of pointer programs using monadic second-order logic

  1997influential reference
• Construction of Abstract State Graphs with PVS

  1997cited by this paper
• Shape types

  1997cited by this paper
• Static detection of dynamic memory errors

  1996cited by this paper
• Compiler-based prefetching for recursive data structures

  1996cited by this paper
• Solving shape-analysis problems in languages with destructive updating

  1996cited by this paper
• POSITION STATEMENT.

  1995cited by this paper
• Incremental and Decremental Evaluation of Transitive Closure by First-Order Queries

  1995influential reference
• Symmetry and Induction in Model Checking

  1995cited by this paper
• Interprocedural may-alias analysis for pointers: beyond k-limiting

  1994cited by this paper
• Analysis of recursive types in an imperative language

  1994cited by this paper
• Interprocedural heap analysis for parallelizing imperative programs

  1993cited by this paper
• Analysis of Dynamic Structures for Efficient Parallel Execution

  1993cited by this paper
• Symmetry and model checking

  1993cited by this paper
• A Lattice for Abstract Interpretation of Dynamic (LISP-Like) Structures

  1992influential reference
• Abstractions for recursive pointer data structures: improving the analysis and transformation of imperative programs

  1992cited by this paper
• A storeless model of aliasing and its abstractions using finite representations of right-regular equivalence relations

  1992cited by this paper
• Abstractions for Recursive Pointer Data Structures: Improving the Analysis of Imperative Programs

  1992cited by this paper
• Abstractions for recursive pointer data structures

  1992cited by this paper
• Pointer-induced aliasing: a problem classification

  1991cited by this paper
• Analysis of pointers and structures

  1990cited by this paper
• A Logic-Based Approach to Data Flow Analysis Problem

  1990cited by this paper
• Parallelizing Programs with Recursive Data Structures

  1989cited by this paper
• Dependence analysis for pointer variables

  1989cited by this paper
• Detecting conflicts between structure accesses

  1988cited by this paper
• Multivalued logics: a uniform approach to reasoning in artificial intelligence

  1988cited by this paper
• Computational Geometry

  1985cited by this paper
• A flexible approach to interprocedural data flow analysis and programs with recursive data structures

  1982cited by this paper
• Assignment and Linked Data Structures

  1982influential reference
• An Introduction to the PL/CV2 Programming Logic

  1982cited by this paper
• Systematic design of program analysis frameworks

  1979cited by this paper
• Flow analysis and optimization of LISP-like structures

  1979influential reference
• Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints

  1977cited by this paper
• A course in mathematical logic

  1977cited by this paper
• A Discipline of Programming

  1976cited by this paper
• An interactive program verifier

  1973cited by this paper
• A Program Verifier

  1971cited by this paper
• Introduction to Metamathematics

  1952cited by this paper

• Automated Verification of Monotonic Data Structure Traversals in C

  2025cites this paper
• Verifying Tree-Manipulating Programs via CHCs

  2025cites this paper
• Universal Synthesis of Differentiably Tunable Numerical Abstract Transformers

  2025cites this paper
• Automated Verification of Tree-Manipulating Programs Using Constrained Horn Clauses

  2024cites this paper
• To Tag, or Not to Tag: Translating C’s Unions to Rust’s Tagged Unions

  2024cites this paper
• Sound Static Analysis for Microservices: Utopia? A Preliminary Experience with LiSA

  2024cites this paper
• Inference of access policies through static analysis

  2024cites this paper
• Practical Verification of Smart Contracts using Memory Splitting

  2024cites this paper
• Tree-Verifiable Graph Grammars

  2024cites this paper
• Concretization of Abstract Traffic Scene Specifications Using Metaheuristic Search

  2023cites this paper
• UNIVERSITY OF CALIFORNIA RIVERSIDE Concolic Testing of Programs with Concurrent Dynamic Data Structures A Dissertation submitted in partial satisfaction of the requirements for the degree of Doctor of Philosophy

  2023cites this paper
• A General Noninterference Policy for Polynomial Time

  2023cites this paper
• An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification

  2023cites this paper
• Low-Level Bi-Abduction

  2022cites this paper
• A Verified Implementation of B+-Trees in Isabelle/HOL

  2022cites this paper
• Project-Team VerTeCs Verification models and techniques applied to the Testing and Control of reactive Systems

  2022cites this paper
• Shape-Analysis Driven Memory Graph Visualization

  2022cites this paper
• Anchor: Fast and Precise Value-flow Analysis for Containers via Memory Orientation

  2022cites this paper
• Symbolic Abstract Heaps for Polymorphic Information-flow Guard Inference (Extended Version)

  2022cites this paper
• Learning Generalized Policy Classes for Stochastic Shortest Path Problems

  2022cites this paper
• A Unifying Approach for Control-Flow-Based Loop Abstraction

  2022cites this paper
• Preliminary Results on Using Abstract AND-OR Graphs for Generalized Solving of Stochastic Shortest Path Problems

  2022cites this paper
• An Automated Analyzer for Financial Security of Ethereum Smart Contracts

  2022cites this paper
• Complexity-guided container replacement synthesis

  2022cites this paper
• Generalized Linear Integer Numeric Planning

  2022cites this paper
• Learning Generalized Policy Automata for Relational Stochastic Shortest Path Problems

  2022cites this paper
• Automated generation of consistent models using qualitative abstractions and exploration strategies

  2021cites this paper
• Verification of Program Transformations with Inductive Refinement Types

  2021influential citation
• Efficient Path-Sensitive Data-Dependence Analysis

  2021cites this paper
• Quantum abstract interpretation

  2021cites this paper
• Worst-Case Execution Time Calculation for Query-Based Monitors by Witness Generation

  2021cites this paper
• DSGEN: concolic testing GPU implementations of concurrent dynamic data structures

  2021cites this paper
• Project-Team VerTeCs Verification models and techniques applied to the Testing and Control of reactive Systems

  2021cites this paper
• Automated reasoning and randomization in separation logic

  2020cites this paper
• Verified Textbook Algorithms - A Biased Survey

  2020cites this paper
• Refinement Types: A Tutorial

  2020cites this paper
• Learning the boundary of inductive invariants

  2020cites this paper
• Refinement Types: A Tutorial

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

  2020cites this paper
• Learning Generalized Relational Heuristic Networks for Model-Agnostic Planning

  2020cites this paper
• No Crash, No Exploit: Automated Verification of Embedded Kernels

  2020cites this paper
• Bi-Abduction for Shapes with Ordered Data

  2020cites this paper
• A study of learning likely data structure properties using machine learning models

  2020cites this paper
• Semantic prefetching using forecast slices

  2020cites this paper
• Scalable pointer analysis of data structures using semantic models

  2020cites this paper
• A Survey on Heap Analysis

  2020cites this paper
• Automatically Proving Microkernels Free from Privilege Escalation from their Executable

  2020cites this paper
• A Learning-Based Approach to Synthesizing Invariants for Incomplete Verification Engines

  2020cites this paper
• Predicate Extension of Symbolic Memory Graphs for the Analysis of Memory Safety Correctness

  2020cites this paper
• Data-driven inference of representation invariants

  2020cites this paper
• Analogy-making as a Core primitive in the software engineering toolbox

  2020cites this paper
• Pointer Data Structure Synthesis from Answer Set Programming Specifications

  2020cites this paper
• Bi-Abductive Inference for Shape and Ordering Properties

  2019cites this paper
• 1 Deciding Memory Safety for Forest Datastructures

  2019cites this paper
• Predicate extension of symbolic memory graphs for analysis of memory safety correctness

  2019cites this paper
• Synchronized pushdown systems for pointer and data-flow analysis

  2019cites this paper
• A Study of Learning Data Structure Invariants Using Off-the-shelf Tools

  2019cites this paper
• Habilitation à Diriger des Recherches Xavier Rival Domaines Abstraits pour l ’ Analyse Statique de Programmes Manipulant des Structures de Données Complexes Abstract Domains for the Static Analysis of Programs Manipulating Complex Data Structures

  2019influential citation
• Automatic verification of heap-manipulating programs

  2019cites this paper
• Deciding Memory Safety for Forest Datastructures

  2019cites this paper
• Compositional Verification of Heap-Manipulating Programs through Property-Guided Learning

  2019cites this paper
• Scalable logic defined static analysis

  2019cites this paper
• Sub-Turing Islands in the Wild

  2019cites this paper
• Generalized Planning via Abstraction: Arbitrary Numbers of Objects

  2019cites this paper
• Towards an abstraction for data structures that implement cooperation mechanisms

  2019cites this paper
• Computing the Scope of Applicability for Acquired Task Knowledge in Experience-Based Planning Domains

  2019cites this paper
• Learning Task Knowledge and its Scope of Applicability in Experience-Based Planning Domains

  2019influential citation
• Pretend synchrony: synchronous verification of asynchronous distributed programs

  2019cites this paper
• Unsupervised learning of API aliasing specifications

  2019cites this paper
• Abstract Heap Relations for a Compositional Shape Analysis. (Abstractions Relationnelles de la Mémoire pour une Analyse Compositionnelle de Structures de Données)

  2019cites this paper
• Comparative Analysis of Approaches to Static Verification of Dynamic Memory

  2019influential citation
• Analysis and Abstraction of Graph Transformation Systems via Type Graphs

  2019cites this paper
• Dynamically Allocated Memory Verification in Object-Oriented Programs using Prolog

  2019cites this paper
• Deciding memory safety for single-pass heap-manipulating programs

  2019influential citation
• PrideMM: Second Order Model Checking for Memory Consistency Models

  2019cites this paper
• Compositional Abstractions for Verifying Concurrent Data Structures

  2019cites this paper
• Learning the Scope of Applicability for Task Planning Knowledge in Experience-Based Planning Domains

  2019influential citation
• Software Engineering Tools: Compatability and Integration

  2019cites this paper
• Programming Languages and Systems: 17th Asian Symposium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1–4, 2019, Proceedings

  2019cites this paper
• Combining Model Checking and Data-Flow Analysis

  2018cites this paper
• Formal verification-driven parallelisation synthesis

  2018cites this paper
• Multi-valued Logic for Static Analysis and Model Checking

  2018cites this paper
• A Thread Modularity Approach for Verification Concurrent Software Based on Abstract Interpretation

  2018cites this paper
• Evaluating Design Tradeoffs in Numeric Static Analysis for Java

  2018cites this paper
• Constraint-Based Thread-Modular Abstract Interpretation

  2018cites this paper
• An efficient data structure for must-alias analysis

  2018cites this paper
• Fragment Abstraction for Concurrent Shape Analysis

  2018cites this paper
• Precise Reasoning with Structured Heaps and Collective Operations à la Map / Reduce What Static Analysis can Learn From High-Performance DSLs

  2018cites this paper
• Shape Abstractions with Support for Sharing and Disjunctions. (Abstractions de la Forme des Structures de Données Supportant Partage et Disjonctions)

  2018cites this paper
• A Theoretical Foundation of Sensitivity in an Abstract Interpretation Framework

  2018cites this paper
• Automatic Verification of Embedded System Code Manipulating Dynamic Structures Stored in Contiguous Regions

  2018cites this paper
• To Memory Safety through Proofs

  2018cites this paper
• Efficient Verification of Programs with Complex Data Structures Using SMT Solvers

  2018cites this paper
• Template-Based Verification of Heap-Manipulating Programs

  2018cites this paper
• Computing the Spatial Probability of Inclusion inside Partial Contours for Computer Vision Applications

  2018cites this paper
• From Jinja bytecode to term rewriting: A complexity reflecting transformation

  2018cites this paper
• Combining Symbolic and Numerical Domains for Information Leakage Analysis

  2018influential citation
• Synchronous Verification of Asynchronous Distributed Programs

  2018cites this paper
• Why Separation Logic Works

  2018cites this paper
• Abstraction and Abstraction Refinement

  2018cites this paper