:: Library Catalog

Cover Image

Saved in:

Bibliographic Details
Main Authors:	Wu, Haoze, Barrett, Clark, Narodytska, Nina
Format:	Preprint
Published:	2025
Subjects:	Logic in Computer Science
Online Access:	https://arxiv.org/abs/2504.19039
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Lemur: Integrating Large Language Models in Automated Program Verification
by: Wu, Haoze, et al.
Published: (2023)

Viverra: Text-to-Code with Guarantees
by: Wu, Haoze, et al.
Published: (2026)

SpotIt+: Verification-based Text-to-SQL Evaluation with Database Constraints
by: Tremante, Andrew, et al.
Published: (2026)

SpotIt: Evaluating Text-to-SQL Evaluation with Formal Verification
by: Klopfenstein, Rocky, et al.
Published: (2025)

Proof Minimization in Neural Network Verification
by: Isac, Omri, et al.
Published: (2025)

PICID: Proof-Driven Clause Learning in Neural Network Verification
by: Isac, Omri, et al.
Published: (2025)

The nonexistence of unicorns and many-sorted Löwenheim-Skolem theorems
by: Przybocki, Benjamin, et al.
Published: (2024)

Satisfiability Modulo Extensional Constant Arrays (Extended Version)
by: Preiner, Mathias, et al.
Published: (2026)

Generalized Optimization Modulo Theories
by: Tsiskaridze, Nestan, et al.
Published: (2024)

Lean-auto: An Interface between Lean 4 and Automated Theorem Provers
by: Qian, Yicheng, et al.
Published: (2025)

Automating Bitvector and Finite Field Equivalence Proofs in Lean
by: Pertseva, Elizaveta, et al.
Published: (2026)

Verifying SQL Queries using Theories of Tables and Relations
by: Mohamed, Mudathir, et al.
Published: (2024)

The termination of Nielsen transformations applied to word equations with length constraints
by: Przybocki, Benjamin, et al.
Published: (2025)

Satisfiability Modulo Theories for Verifying MILP Certificates
by: Wood, Kenan, et al.
Published: (2023)

Nazrin: Atomic Tactics for Graph Neural Networks for Theorem Proving in Lean 4
by: Aniva, Leni, et al.
Published: (2026)

Solving Set Constraints with Comprehensions and Bounded Quantifiers
by: Mohamed, Mudathir, et al.
Published: (2025)

Incremental Neural Network Verification via Learned Conflicts
by: Elsaleh, Raya, et al.
Published: (2026)

Relational Hoare Logic for Realistically Modelled Machine Code
by: Mazzucato, Denis, et al.
Published: (2025)

Integer Reasoning Modulo Different Constants in SMT
by: Pertseva, Elizaveta, et al.
Published: (2025)

Towards SMT Solver Stability via Input Normalization
by: Amrollahi, Daneshvar, et al.
Published: (2024)

Cube-based Isomorph-free Finite Model Finding
by: Chow, Choiwah, et al.
Published: (2025)

Concept-based Analysis of Neural Networks via Vision-Language Models
by: Mangal, Ravi, et al.
Published: (2024)

Lean-SMT: An SMT tactic for discharging proof goals in Lean
by: Mohamed, Abdalrhman, et al.
Published: (2025)

The Modal Cube Revisited: Semantics without Worlds (Technical Report)
by: Leme, Renato, et al.
Published: (2025)

Safe and Reliable Training of Learning-Based Aerospace Controllers
by: Mandal, Udayan, et al.
Published: (2024)

Abstraction-Based Proof Production in Formal Verification of Neural Networks
by: Elboher, Yizhak Yisrael, et al.
Published: (2025)

On the Interplay of Cube Learning and Dependency Schemes in QCDCL Proof Systems
by: Choudhury, Abhimanyu, et al.
Published: (2025)

Efficiently Synthesizing Lowest Cost Rewrite Rules for Instruction Selection
by: Daly, Ross, et al.
Published: (2024)

Marabou 2.0: A Versatile Formal Analyzer of Neural Networks
by: Wu, Haoze, et al.
Published: (2024)

CSLib: The Lean Computer Science Library
by: Barrett, Clark, et al.
Published: (2026)

Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4
by: Aniva, Leni, et al.
Published: (2024)

The Luna Bound Propagator for Formal Analysis of Neural Networks
by: LeCates, Henry, et al.
Published: (2026)

Gödel Incompleteness Theorem for PAC Learnable Theory from the view of complexity measurement
by: Ma, Zhifeng, et al.
Published: (2024)

The Parameterized Complexity of Learning Monadic Second-Order Logic
by: van Bergerem, Steffen, et al.
Published: (2023)

Equivalence Hypergraphs: DPO Rewriting for Monoidal E-Graphs
by: Tiurin, Aleksei, et al.
Published: (2024)

Stokes' Theorem for Smooth Singular Cubes in Lean 4: True Pullback, Bridges to mathlib4, and Chain-Level d^2=0
by: Hulak, David B., et al.
Published: (2026)

Sequent Calculi for Data-Aware Modal Logics
by: Areces, Carlos, et al.
Published: (2025)

Comparing and Contrasting Arrow's Impossibility Theorem and Gödel's Incompleteness Theorem
by: Livson, Ori, et al.
Published: (2025)

A study of cut-elimination for a non-labelled cyclic proof system for propositional dynamic logics
by: Oda, Yukihiro
Published: (2025)

Abstract computation over first-order structures. Part IIa: Moschovakis' operator and other non-determinisms
by: Gaßner, Christine
Published: (2025)