Cover Image

Verifying Solutions to Semantics-Guided Synthesis Problems

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Murphy, Charlie, Johnson, Keith, Reps, Thomas, D'Antoni, Loris
Format:	Preprint
Published:	2024
Subjects:	Programming Languages Logic in Computer Science
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)

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

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

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

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

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

Realizability in Semantics-Guided Synthesis Done Eagerly
by: Meyer, Roland, et al.
Published: (2024)

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

Automating Unrealizability Logic: Hoare-Style Proof Synthesis for Infinite Sets of Programs
by: Nagy, Shaan, et al.
Published: (2024)

Verifying Lock-free Search Structure Templates
by: Patel, Nisarg, et al.
Published: (2024)

Pragmatics of Formally Verified Yet Efficient Static Analysis, in particular for Formally Verified Compilers
by: Monniaux, David
Published: (2024)

Verifying Floating-Point Programs in Stainless
by: Gilot, Andrea, et al.
Published: (2026)

An Introduction to Different Approaches to Initial Semantics
by: Lamiaux, Thomas, et al.
Published: (2024)

Verifying Peephole Rewriting In SSA Compiler IRs
by: Bhat, Siddharth, et al.
Published: (2024)

Verifying Functional Correctness Properties At the Level of Java Bytecode
by: Paganoni, Marco, et al.
Published: (2024)

A Formally Verified Procedure for Width Inference in FIRRTL
by: Wang, Keyin, et al.
Published: (2026)

Logical Relations for Formally Verified Authenticated Data Structures
by: Gregersen, Simon Oddershede, et al.
Published: (2025)

A Formalization of the Yul Language and Some Verified Yul Code Transformations
by: Coglio, Alessandro, et al.
Published: (2025)

Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library
by: de Vilhena, Paulo Emílio, et al.
Published: (2021)

Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach (Extended Version)
by: Grandury, Marcos, et al.
Published: (2025)

Semantically Reflected Programs
by: Kamburjan, Eduard, et al.
Published: (2025)

Denotational Semantics for Probabilistic and Concurrent Programs
by: Zilberstein, Noam, et al.
Published: (2025)

Wiring the Pi-calculus to Denotational Semantics
by: Sakayori, Ken, et al.
Published: (2026)

Disentangling Parallelism and Interference in Game Semantics
by: Castellan, Simon, et al.
Published: (2021)

Provenance Guided Rollback Suggestions
by: Zhao, David, et al.
Published: (2025)

Useful Evaluation: Syntax and Semantics (Technical Report)
by: Barenbaum, Pablo, et al.
Published: (2024)

An Encoding for CLP Problems in SMT-LIB
by: Amrollahi, Daneshvar, et al.
Published: (2024)

Foundations of Digital Circuits: Denotation, Operational, and Algebraic Semantics
by: Kaye, George
Published: (2025)

Logical Predicates in Higher-Order Mathematical Operational Semantics
by: Goncharov, Sergey, et al.
Published: (2024)

A Coq Library of Sets for Teaching Denotational Semantics
by: Cao, Qinxiang, et al.
Published: (2024)

Token-Sensitive Enclosure Semantics for Measurement-Bearing Expressions
by: Hulak, David B., et al.
Published: (2026)

A Formal Semantics of the GraalVM Intermediate Representation
by: Webb, Brae J., et al.
Published: (2021)

Towards a Higher-Order Bialgebraic Denotational Semantics
by: Goncharov, Sergey, et al.
Published: (2026)

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

Syntax-Guided Automated Program Repair for Hyperproperties
by: Beutner, Raven, et al.
Published: (2024)

A Unified Framework for Initial Semantics
by: Lamiaux, Thomas, et al.
Published: (2025)

Critical Sections Are Not Per-Thread: A Trace Semantics for Lock-Based Concurrency
by: Sulzmann, Martin
Published: (2026)

Verifying Asynchronous Hyperproperties in Reactive Systems
by: Beutner, Raven, et al.
Published: (2025)

CIll: CTI-Guided Invariant Generation via LLMs for Model Checking
by: Su, Yuheng, et al.
Published: (2026)

Breaking the Mold: Nonlinear Ranking Function Synthesis Without Templates
by: Zhu, Shaowei, et al.
Published: (2024)