Introduces token-sensitive enclosure semantics where each measurement carries an interval and an observation token, defining warranted enclosures as sets of consistent values, with proofs that token-erased summaries cannot recover correct rewrite classes, all mechanized in Lean 4.
hub
Abstract interpretation: A un ified lattice model for static analysis of programs by construction or app roximation of fixpoints
16 Pith papers cite this work, alongside 6,191 external citations. Polarity classification is still indexing.
16
Pith papers citing it
6,191
external citations · external index
hub tools
citation-role summary
background 1
citation-polarity summary
roles
background 1polarities
background 1representative citing papers
APPL is a sound, relatively complete abstract program logic that subsumes Hoare, incorrectness, and hyperproperty logics via lattice semantics and a non-idempotent monoidal operator for nondeterminism.
GNTC satisfiability is 2-EXPTIME-complete and GNTC model checking is P^{NP[O(log^2 n)]}-complete, settling open bounds for UNTC and UNFO^reg.
Agentic interpretation uses lattices to track LLM judgments on decomposed program claims during analysis.
Presynthesis constructs a tree automaton and oracle offline to allow efficient use of fine-grained abstract semantics for pruning in search-based program synthesis.
A new abstract interpretation algorithm enables sound optimistic analysis of e-graphs during equality saturation, unifying it with non-destructive rewriting and improving precision on cyclic SSA programs.
Presents Evolving Abstract Transformers with UPOSE and AGG algorithms to create adaptable, domain-agnostic sound transformers for polyhedral abstract domains in program analysis.
BEC is a bit-level static analysis implemented in LLVM that classifies register bit corruptions to prune up to 30% of fault-injection campaigns and reduce program vulnerability by up to 13% via bit-aware instruction scheduling on RISC-V.
GIF introduces a Jacobian-based upper bound on input-output mutual information in LLMs with formal Lean proof and strong empirical recall on injection and leakage benchmarks.
A systematic mapping study of 248 papers introduces a taxonomy of synergistic effects, inter-analysis workflows, and mapping functions to catalog patterns in combined program analysis techniques.
LORIS detects local reasoning errors in LLM-generated proofs for loop invariants by translating natural-language steps to first-order logic implications and using invalid implications to refine the invariants, achieving 93.1% success on 460 C programs.
A linear-time randomized static analysis that propagates constant-width bitstrings enables phase folding and T-count optimization matching SOTA tools on large circuits.
SAQR-QC is a new logic for scalable approximate quantitative reasoning about quantum circuits via local qubit operations and controlled precision loss, demonstrated on GHZ circuits and quantum phase estimation.
The authors perform and analyze three reformalizations of the Jordan Curve Theorem from Mizar to Lean, HOL Light to Lean, and HOL Light to Agda.
Ranger is a bidirectional refinement type system for integer range types, implemented in the Licorne language, that integrates inference and flow analysis to verify bounds properties with low annotation overhead compared to Java, Scala, Checker Framework, and Liquid Java.
An empirical study finds that injecting call/inheritance topology as comments improves LLM code agent localization by 2.2pp, shortens trajectories by 1.6 rounds, and halves run-to-run variance on medium repositories via a deterministic anchoring effect.
citing papers explorer
-
Token-Sensitive Enclosure Semantics for Measurement-Bearing Expressions
Introduces token-sensitive enclosure semantics where each measurement carries an interval and an observation token, defining warranted enclosures as sets of consistent values, with proofs that token-erased summaries cannot recover correct rewrite classes, all mechanized in Lean 4.
-
A Program Logic for Abstract (Hyper)Properties
APPL is a sound, relatively complete abstract program logic that subsumes Hoare, incorrectness, and hyperproperty logics via lattice semantics and a non-idempotent monoidal operator for nondeterminism.
-
Guarded Negation Transitive Closure Logic
GNTC satisfiability is 2-EXPTIME-complete and GNTC model checking is P^{NP[O(log^2 n)]}-complete, settling open bounds for UNTC and UNFO^reg.
-
Agentic Interpretation: Lattice-Structured Evidence for LLM-Based Program Analysis
Agentic interpretation uses lattices to track LLM judgments on decomposed program claims during analysis.
-
Presynthesis: Towards Scaling Up Program Synthesis with Finer-Grained Abstract Semantics
Presynthesis constructs a tree automaton and oracle offline to allow efficient use of fine-grained abstract semantics for pruning in search-based program synthesis.
-
Optimism in Equality Saturation
A new abstract interpretation algorithm enables sound optimistic analysis of e-graphs during equality saturation, unifying it with non-destructive rewriting and improving precision on cyclic SSA programs.
-
Evolving Abstract Transformers for Gradient-Guided, Adaptable Abstract Interpretation
Presents Evolving Abstract Transformers with UPOSE and AGG algorithms to create adaptable, domain-agnostic sound transformers for polyhedral abstract domains in program analysis.
-
BEC: Bit-Level Static Analysis for Reliability against Soft Errors
BEC is a bit-level static analysis implemented in LLVM that classifies register bit corruptions to prune up to 30% of fault-injection campaigns and reduce program vulnerability by up to 13% via bit-aware instruction scheduling on RISC-V.
-
GIF: Locally Sound Geometric Information Flow Control for LLMs
GIF introduces a Jacobian-based upper bound on input-output mutual information in LLMs with formal Lean proof and strong empirical recall on injection and leakage benchmarks.
-
Combined Program Analysis Techniques: A Systematic Mapping Study
A systematic mapping study of 248 papers introduces a taxonomy of synergistic effects, inter-analysis workflows, and mapping functions to catalog patterns in combined program analysis techniques.
-
Guiding LLM-based Loop Invariant Synthesis via Feedback on Local Reasoning Errors
LORIS detects local reasoning errors in LLM-generated proofs for loop invariants by translating natural-language steps to first-order logic implications and using invalid implications to refine the invariants, achieving 93.1% success on 460 C programs.
-
Linear-Time T-Gate Optimization via Random Abstraction
A linear-time randomized static analysis that propagates constant-width bitstrings enables phase folding and T-count optimization matching SOTA tools on large circuits.
-
SAQR-QC: A Logic for Scalable but Approximate Quantitative Reasoning about Quantum Circuits
SAQR-QC is a new logic for scalable approximate quantitative reasoning about quantum circuits via local qubit operations and controlled precision loss, demonstrated on GHZ circuits and quantum phase estimation.
-
Reformalization of the Jordan Curve Theorem
The authors perform and analyze three reformalizations of the Jordan Curve Theorem from Mizar to Lean, HOL Light to Lean, and HOL Light to Agda.
-
Practical Range Refinement Types with Inference
Ranger is a bidirectional refinement type system for integer range types, implemented in the Licorne language, that integrates inference and flow analysis to verify bounds properties with low annotation overhead compared to Java, Scala, Checker Framework, and Liquid Java.
-
How Much Static Structure Do Code Agents Need? A Study of Deterministic Anchoring
An empirical study finds that injecting call/inheritance topology as comments improves LLM code agent localization by 2.2pp, shortens trajectories by 1.6 rounds, and halves run-to-run variance on medium repositories via a deterministic anchoring effect.