6 papers
Elusive but Coverable: The Recursion-Theoretic Structure of Complete Abstract Interpretations
Nicklas Carpenter, Roberto Giacobazzi
We study local completeness and incompleteness of abstract interpretations from a recursion-theoretic perspective. Local completeness weakens global completeness and captures the a…
Sound up-to techniques and Complete abstract domains
Filippo Bonchi, Pierre Ganty, Roberto Giacobazzi +1
Abstract interpretation is a method to automatically find invariants of programs or pieces of code whose semantics is given via least fixed-points. Up-to techniques have been intro…
SEA: String Executability Analysis by Abstract Interpretation
Vincenzo Arceri, Mila Dalla Preda, Roberto Giacobazzi +1
Dynamic languages often employ reflection primitives to turn dynamically generated text into executable code at run-time. These features make standard static analysis extremely har…
Correctness Kernels of Abstract Interpretations
Roberto Giacobazzi, Francesco Ranzato
In abstract interpretation-based static analysis, approximation is encoded by abstract domains. They provide systematic guidelines for designing abstract semantic functions that ap…
Incompleteness of States w.r.t. Traces in Model Checking
Roberto Giacobazzi, Francesco Ranzato
Cousot and Cousot introduced and studied a general past/future-time specification language, called mu*-calculus, featuring a natural time-symmetric trace-based semantics. The stand…
Making Abstract Domains Condensing
R. Giacobazzi, F. Ranzato, F. Scozzari
In this paper we show that reversible analysis of logic languages by abstract interpretation can be performed without loss of precision by systematically refining abstract domains.…