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
14 Pith papers cite this work. Polarity classification is still indexing.
14
Pith papers citing it
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.
A randomized linear-time phase-folding algorithm using constant-width bitstring abstraction optimizes T-count in quantum circuits orders of magnitude faster than prior tools while achieving comparable reductions.
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.
GNTC satisfiability is 2ExpTime-complete and model checking is P^NP[O(log² n)]-complete via polynomial and exponential reductions to UNTC and 2-way alternating parity tree automata.
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.
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.
Lightweight call and inheritance topology injected as comments improves function localization by 2.2pp, shortens trajectories, and halves run-to-run variance in LLM code agents, with benefits depending on repository scale.
citing papers explorer
-
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.