Cover Image

Automating Unrealizability Logic: Hoare-Style Proof Synthesis for Infinite Sets of Programs

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Nagy, Shaan, Kim, Jinwoo, Reps, Thomas, D'Antoni, Loris
Format:	Preprint
Published:	2024
Subjects:	Programming Languages
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

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

Semantics of Sets of Programs
by: Kim, Jinwoo, et al.
Published: (2024)

Automating Pruning in Top-Down Enumeration for Program Synthesis Problems with Monotonic Semantics
by: Johnson, Keith J. C., et al.
Published: (2024)

Synthesizing Specifications
by: Park, Kanghee, et al.
Published: (2023)

Verifying Solutions to Semantics-Guided Synthesis Problems
by: Murphy, Charlie, et al.
Published: (2024)

ChopChop: a Programmable Framework for Semantically Constraining the Output of Language Models
by: Nagy, Shaan, et al.
Published: (2025)

The SemGuS Toolkit
by: Johnson, Keith J. C., et al.
Published: (2024)

Synthesizing Formal Semantics from Executable Interpreters
by: Liu, Jiangyi, et al.
Published: (2024)

LOUD: Synthesizing Strongest and Weakest Specifications
by: Park, Kanghee, et al.
Published: (2024)

Cyclic Proofs in Hoare Logic and its Reverse
by: Brotherston, James, et al.
Published: (2025)

Language-Based Agent Control
by: Zhou, Timothy, et al.
Published: (2026)

Bootstrapping Fuzzers for Compilers of Low-Resource Language Dialects Using Language Models
by: Vaidya, Sairam, et al.
Published: (2025)

Continuous Diffusion Models Can Obey Formal Syntax
by: Kim, Jinwoo, et al.
Published: (2026)

Encode the $\forall\exists$ Relational Hoare Logic into Standard Hoare Logic
by: Wu, Shushu, et al.
Published: (2025)

Newtonian Program Analysis of Probabilistic Programs
by: Wang, Di, et al.
Published: (2023)

A Hoare Logic for Symmetry Properties
by: Mehta, Vaibhav, et al.
Published: (2025)

Towards Definitional Interpreters for Hoare Logics
by: Sun, Ke, et al.
Published: (2026)

Relational Hoare Logic for High-Level Synthesis of Hardware Accelerators
by: Tanaka, Izumi, et al.
Published: (2026)

Nice to Meet You: Synthesizing Practical MLIR Abstract Transformers
by: Peng, Xuanyu, et al.
Published: (2025)

Program Synthesis is $Σ_3^0$-Complete
by: Kim, Jinwoo
Published: (2024)

A One-Layer Decoder-Only Transformer is a Two-Layer RNN: With an Application to Certified Robustness
by: Zhang, Yuhao, et al.
Published: (2024)

Gradual Exact Logic: Unifying Hoare Logic and Incorrectness Logic via Gradual Verification
by: Zimmerman, Conrad, et al.
Published: (2024)

SAQR-QC: A Logic for Scalable but Approximate Quantitative Reasoning about Quantum Circuits
by: Yu, Nengkun, et al.
Published: (2025)

Proof systems for partial incorrectness logic (partial reverse Hoare logic)
by: Oda, Yukihiro
Published: (2025)

Flexible and Efficient Grammar-Constrained Decoding
by: Park, Kanghee, et al.
Published: (2025)

A Practical Quantum Hoare Logic with Classical Variables, I
by: Ying, Mingsheng
Published: (2024)

The Format Tax
by: Lee, Ivan Yee, et al.
Published: (2026)

Synthesizing Abstract Transformers for Reduced-Product Domains
by: Kalita, Pankaj Kumar, et al.
Published: (2024)

Hoare meets Heisenberg: A Lightweight Logic for Quantum Programs
by: Sundaram, Aarthi, et al.
Published: (2021)

Software Model Checking via Summary-Guided Search (Extended Version)
by: Fang, Ruijie, et al.
Published: (2025)

Learning the Error Patterns of Language Models
by: Kim, Jinwoo, et al.
Published: (2026)

Scalable Equivalence Checking and Verification of Shallow Quantum Circuits
by: Yu, Nengkun, et al.
Published: (2025)

Efficient Cost Bounds with Linear Maps
by: Kahn, David M, et al.
Published: (2025)

From Program Logics to Language Logics
by: Cimini, Matteo
Published: (2024)

Constrained Adaptive Rejection Sampling
by: Parys, Paweł, et al.
Published: (2025)

A Taxonomy of Hoare-Like Logics: Towards a Holistic View using Predicate Transformers and Kleene Algebras with Top and Tests
by: Verscht, Lena, et al.
Published: (2024)

Automating Equational Proofs in Dirac Notation
by: Xu, Yingte, et al.
Published: (2024)

Agentic Proof Automation: A Case Study
by: Xu, Yichen, et al.
Published: (2026)

Functional Logic Program Transformations
by: Hanus, Michael, et al.
Published: (2026)

Formalization and Implementation of Safe Destination Passing in Pure Functional Programming Settings
by: Bagrel, Thomas
Published: (2026)