Abstract interpretation with alien expressions and heap structures

DOI10.1007/978-3-540-30579-8_11MaRDI QIDQ5711488zbMATH OpenOpenAlexFDO

Authors Bor-Yuh Evan Chang, K. Rustan M. Leino

Publication date 6 December 2005

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b105073

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

Recommendations

• An Abstract Domain for Analyzing Heap-Manipulating Low-Level Software
• Comparison of abstract interpretations
• Abstract domains for universal and existential properties
• Class analysis of object-oriented programs through abstract interpretation
• Partially disjunctive heap abstraction

Cited in

(16)

• A lattice for abstract interpretation of dynamic (LISP-like) structures
• The map equality domain
• Recognition of logically related regions based heap abstraction
• Program verification with interacting analysis plugins
• Class analysis of object-oriented programs through abstract interpretation
• A generic framework for heap and value analyses of object-oriented programming languages
• A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis
• Inferring Loop Invariants Using Postconditions
• Abstract cofibered domains: application to the alias analysis of untyped programs
• Loop invariants: analysis, classification, and examples
• Formalisation and implementation of an algorithm for bytecode verification of \@NonNull types
• An Abstract Domain for Analyzing Heap-Manipulating Low-Level Software
• A Flexible, (C)LP-Based Approach to the Analysis of Object-Oriented Programs
• Symbolic abstract heaps for polymorphic information-flow guard inference
• Fast approximations of quantifier elimination
• Context-sensitive meta-constraint systems for explainable program analysis

This page was built for publication: Abstract interpretation with alien expressions and heap structures

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5711488)