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.
Abstract interpretation: A un ified lattice model for static analysis of programs by construction or app roximation of fixpoints,
12 Pith papers cite this work. Polarity classification is still indexing.
12
Pith papers citing it
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.
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.
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.
-
Linear-Time T-Gate Optimization via Random Abstraction
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: 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.
-
Guarded Negation Transitive Closure Logic
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: 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.
-
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.
-
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.