Making abstract interpretations complete

DOI10.1145/333979.333989zbMath1133.68370OpenAlexW2046160987MaRDI QIDQ5385340

Francesca Scozzari, Roberto Giacobazzi, Francesco Ranzato

Publication date: 5 May 2008

Published in: Journal of the ACM (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/333979.333989

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Abstract Program Slicing ⋮ Code obfuscation against abstraction refinement attacks ⋮ Lattice-based refinement in bounded model checking ⋮ Why does Astrée scale up? ⋮ Optimality in goal-dependent analysis of Sharing ⋮ Abstract domains for type juggling ⋮ On collecting semantics for program analysis ⋮ Fixpoint Theory -- Upside Down ⋮ Inverse-limit and topological aspects of abstract interpretation ⋮ Deciding program properties via complete abstractions on bounded domains ⋮ Property-driven code obfuscations reinterpreting Jones-optimality in abstract interpretation ⋮ Local completeness logic on Kleene algebra with tests ⋮ Complete Abstractions and Subclassical Modal Logics ⋮ An abstract interpretation framework for genotype elimination algorithms ⋮ Transforming Abstract Interpretations by Abstract Interpretation ⋮ Semantics-based software watermarking by abstract interpretation ⋮ Abstract interpretation of database query languages ⋮ Control-flow analysis of function calls and returns by abstract interpretation ⋮ Generalizing the Paige-Tarjan algorithm by abstract interpretation ⋮ An abstract interpretation-based model for safety semantics ⋮ Abstract neural networks ⋮ Formal framework for reasoning about the precision of dynamic analysis ⋮ On multi-language abstraction. Towards a static analysis of multi-language programs ⋮ Twinning automata and regular expressions for string static analysis ⋮ Combining search space partition and abstraction for LTL model checking ⋮ Maximal incompleteness as obfuscation potency ⋮ 3-valued abstraction: More precision at less cost ⋮ Correctness kernels of abstract interpretations ⋮ Making abstract models complete ⋮ Using abstract interpretation to add type checking for interfaces in Java bytecode verification ⋮ Incompleteness of states w.r.t. traces in model checking ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Abstracting Nash equilibria of supermodular games ⋮ Deriving Bisimulations by Simplifying Partitions ⋮ Internal and External Logics of Abstract Interpretations ⋮ Abstract Interpretation From a Denotational-semantics Perspective ⋮ Cooperative Query Answering by Abstract Interpretation ⋮ Weakening additivity in adjoining closures ⋮ Completeness of string analysis for dynamic languages ⋮ Observational Completeness on Abstract Interpretation ⋮ Abstract Interpretation from a Topological Perspective ⋮ Modelling declassification policies using abstract domain completeness ⋮ Unveiling metamorphism by abstract interpretation of code properties ⋮ A semantic framework for the abstract model checking of tccp programs ⋮ A theory of observables for logic programs ⋮ What You Lose is What You Leak: Information Leakage in Declassification Policies ⋮ Extracting Program Logics From Abstract Interpretations Defined by Logical Relations

This page was built for publication: Making abstract interpretations complete