Neuro-symbolic IC3+LLM framework finds inductive invariants for 29 distributed protocols in TLA+ and proves them inductive via TLAPS.
Title resolution pending
6 Pith papers cite this work. Polarity classification is still indexing.
6
Pith papers citing it
citation-role summary
background 1
citation-polarity summary
years
2026 6verdicts
UNVERDICTED 6roles
background 1polarities
background 1representative citing papers
Backtrackable Inprocessing enables sound inprocessing at arbitrary decision levels in incremental SAT solving and solves about 1.5 times as many difficult bounds on 2017 BMC benchmarks compared to global-level preprocessing.
Quokka# is a Python library that converts quantum circuit analysis tasks into #SAT problems, offering multiple encodings, approximate equivalence checking, and depth-optimal synthesis.
An encoding of Solidity contracts and first-order Hennessy-Milner logic into Lustre enables Kind 2 model checking of complex temporal properties in smart contracts.
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.
CEGARBox++ with KSP-based SAT-shortcuts outperforms CEGARBox++ and KSP alone on modal satisfiability, especially large satisfiable problems, claimed as first effective SAT-tableaux-resolution integration.
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.
-
Backtrackable Inprocessing
Backtrackable Inprocessing enables sound inprocessing at arbitrary decision levels in incremental SAT solving and solves about 1.5 times as many difficult bounds on 2017 BMC benchmarks compared to global-level preprocessing.
-
Quokka#: Quantum Computing with #SAT
Quokka# is a Python library that converts quantum circuit analysis tasks into #SAT problems, offering multiple encodings, approximate equivalence checking, and depth-optimal synthesis.
-
KindHML: formal verification of smart contracts based on Hennessy-Milner logic
An encoding of Solidity contracts and first-order Hennessy-Milner logic into Lustre enables Kind 2 model checking of complex temporal properties in smart contracts.
-
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.
-
Modal CEGAR-tableaux with RECAR and resolution-based SAT-shortcuts
CEGARBox++ with KSP-based SAT-shortcuts outperforms CEGARBox++ and KSP alone on modal satisfiability, especially large satisfiable problems, claimed as first effective SAT-tableaux-resolution integration.