Cover Image

Accelerating Protocol Synthesis and Detecting Unrealizability with Interpretation Reduction

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Egolf, Derek, Tripakis, Stavros
Format:	Preprint
Published:	2025
Subjects:	Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Recursive Program Synthesis from Sketches and Mixed-Quantifier Properties
by: Egolf, Derek, et al.
Published: (2026)

Efficient Synthesis of Symbolic Distributed Protocols by Sketching
by: Egolf, Derek, et al.
Published: (2024)

Can LLMs Perform Synthesis?
by: Egolf, Derek, et al.
Published: (2026)

Towards Language Model Guided TLA+ Proof Automation
by: Zhou, Yuhao, et al.
Published: (2025)

Interactive Safety Verification of Distributed Protocols by Inductive Proof Decomposition
by: Schultz, William, et al.
Published: (2024)

Compositional Inductive Invariant Based Verification of Neural Network Controlled Systems
by: Zhou, Yuhao, et al.
Published: (2023)

Unrealizability Logic
by: Kim, Jinwoo, et al.
Published: (2022)

Explanations for Unrealizability of Infinite-State Safety Shields
by: Rodriguez, Andoni, et al.
Published: (2025)

LTLGuard: Formalizing LTL Specifications with Compact Language Models and Lightweight Symbolic Reasoning
by: Andresel, Medina, et al.
Published: (2026)

Semantic Foundations of Reductive Reasoning
by: Gheorghiu, Alexander V., et al.
Published: (2024)

Witnessed Symmetric Choice and Interpretations in Fixed-Point Logic with Counting
by: Lichter, Moritz
Published: (2022)

Interpretation of Inaccessible Sets in Martin-Löf Type Theory with One Mahlo Universe
by: Takahashi, Yuta
Published: (2024)

Consistent Update Synthesis via Privatized Beliefs
by: Schlögl, Thomas, et al.
Published: (2024)

Synthesising Full-Information Protocols
by: Berwanger, Dietmar, et al.
Published: (2023)

Temporal Hyperproperties for Population Protocols
by: Waldburger, Nicolas, et al.
Published: (2024)

Wait-Only Broadcast Protocols are Easier to Verify
by: Guillou, Lucie, et al.
Published: (2025)

The TPTP Format for Interpretations
by: Sutcliffe, Geoff, et al.
Published: (2024)

Testing Uniform Random Samplers: Methods, Datasets and Protocols
by: Zeyen, Olivier, et al.
Published: (2025)

Accelerating Loops with Arrays
by: Frohn, Florian, et al.
Published: (2026)

On the Complexity of Proving Polyhedral Reductions
by: Amat, Nicolas, et al.
Published: (2023)

Knowledge Problems in Protocol Analysis: Extending the Notion of Subterm Convergent
by: Bunch, Carter, et al.
Published: (2024)

Finding Cut-Offs in Leaderless Rendez-Vous Protocols is Easy
by: Balasubramanian, A. R., et al.
Published: (2020)

Revisiting Stateful Partial-Order Reduction
by: Herbreteau, Frédéric, et al.
Published: (2024)

Concrete Security Bounds for Simulation-Based Proofs of Multi-Party Computation Protocols
by: Sojakova, Kristina, et al.
Published: (2025)

Deductive Verification of Weak Memory Programs with View-based Protocols (extended version)
by: Şakar, Ömer, et al.
Published: (2026)

Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems
by: Ahrens, Emma, et al.
Published: (2025)

Functional Reduction to Speed Up Bounded Model Checking
by: Yu, Changyuan, et al.
Published: (2025)

Integrating Loop Acceleration into Bounded Model Checking
by: Frohn, Florian, et al.
Published: (2024)

Model Checking as Program Verification by Abstract Interpretation (Extended Version)
by: Baldan, Paolo, et al.
Published: (2025)

Reduction Free Normalisation for a proof irrelevant type of propositions
by: Coquand, Thierry
Published: (2021)

Local-Order-Invariant Logic on Classes of Bounded Degree
by: Aoki, Derek
Published: (2025)

Partial Rewriting and Value Interpretation of Logically Constrained Terms (Full Version)
by: Aoto, Takahito, et al.
Published: (2026)

Modular Attractor Acceleration in Infinite-State Games (Full Version)
by: Heim, Philippe, et al.
Published: (2026)

Synthesis with Guided Environments
by: Kupferman, Orna, et al.
Published: (2025)

Program Synthesis in Saturation
by: Hozzová, Petra, et al.
Published: (2024)

Efficient Reactive Synthesis
by: Ye, Xin, et al.
Published: (2024)

Synthesis of Temporal Causality
by: Finkbeiner, Bernd, et al.
Published: (2024)

A Faithful and Quantitative Notion of Distant Reduction for the Lambda-Calculus with Generalized Applications
by: Santo, José Espírito, et al.
Published: (2022)

FORWORD: Accelerating Formal Datapath Verification via Word-Level Sweeping
by: Yang, Ziyi, et al.
Published: (2025)

Formal Verification of the Sumcheck Protocol
by: Bosshard, Azucena Garvía, et al.
Published: (2024)