Neuro-symbolic IC3+LLM framework finds inductive invariants for 29 distributed protocols in TLA+ and proves them inductive via TLAPS.
Wilcox, Eva Darulova, Dan Grossman, and Zachary Tatlock
9 Pith papers cite this work. Polarity classification is still indexing.
9
Pith papers citing it
citation-role summary
background 1
citation-polarity summary
verdicts
UNVERDICTED 9roles
background 1polarities
background 1representative citing papers
An incremental safety proof system using forward-backward reasoning and prophecy steps allows proving safety with simpler invariants than a single complex inductive invariant.
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.
Soteria is a functional library for building direct symbolic execution engines, demonstrated by the first Rust engine supporting Tree Borrows and a compositional C engine that matches or exceeds prior tools.
Presents Evolving Abstract Transformers with UPOSE and AGG algorithms to create adaptable, domain-agnostic sound transformers for polyhedral abstract domains in program analysis.
The paper characterizes forward-mode AD as a unique structure-preserving macro on a higher-order language with ADTs and proves its semantic correctness using a gluing construction on diffeological spaces, extending to higher-order derivatives.
Empirical comparison of equality saturation versus stochastic search on five benchmarks to evaluate if e-graphs are superior for rewrite-based optimization.
EggMind automates EqSat strategy synthesis via LLMs and EqSatL, cutting final cost 45.1% and peak RAM 69.1% versus full equality saturation on vectorization benchmarks while transferring to tensor compilers.
AutoQ 2.0 verifies quantum programs with classical control flow and successfully checks RUS algorithms instantly plus weak-measurement Grover search on 100 qubits in about 20 minutes.
citing papers explorer
-
Synthesizing Inductive Invariants for Distributed Protocols via IC3 and Large Language Models
Neuro-symbolic IC3+LLM framework finds inductive invariants for 29 distributed protocols in TLA+ and proves them inductive via TLAPS.
-
Simplifying Safety Proofs with Forward-Backward Reasoning and Prophecy
An incremental safety proof system using forward-backward reasoning and prophecy steps allows proving safety with simpler invariants than a single complex inductive invariant.
-
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.
-
Soteria: Efficient Symbolic Execution as a Functional Library
Soteria is a functional library for building direct symbolic execution engines, demonstrated by the first Rust engine supporting Tree Borrows and a compositional C engine that matches or exceeds prior tools.
-
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.
-
Higher Order Automatic Differentiation of Higher Order Functions
The paper characterizes forward-mode AD as a unique structure-preserving macro on a higher-order language with ADTs and proves its semantic correctness using a gluing construction on diffeological spaces, extending to higher-order derivatives.
-
Rewrite System Showdown: Stochastic Search vs. EqSat
Empirical comparison of equality saturation versus stochastic search on five benchmarks to evaluate if e-graphs are superior for rewrite-based optimization.
-
LLM-Guided Strategy Synthesis for Scalable Equality Saturation
EggMind automates EqSat strategy synthesis via LLMs and EqSatL, cutting final cost 45.1% and peak RAM 69.1% versus full equality saturation on vectorization benchmarks while transferring to tensor compilers.
-
AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs (Technical Report)
AutoQ 2.0 verifies quantum programs with classical control flow and successfully checks RUS algorithms instantly plus weak-measurement Grover search on 100 qubits in about 20 minutes.