Copertina

A Primal-Dual Perspective on Program Verification Algorithms (Extended Version)

Fuente: arXiv

Salvato in:

Dettagli Bibliografici
Autori principali:	Tsukada, Takeshi, Unno, Hiroshi, Padon, Oded, Shoham, Sharon
Natura:	Preprint
Pubblicazione:	2025
Soggetti:	Programming Languages Logic in Computer Science
Accesso online:	Acceder al recurso
Tags:	Aggiungi Tag Nessun Tag, puoi essere il primo ad aggiungerne!!

Documenti analoghi

An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification
di: Elad, Neta, et al.
Pubblicazione: (2023)

Verifying First-Order Temporal Properties of Infinite-State Systems via Timers and Rankings
di: Lotan, Raz, et al.
Pubblicazione: (2026)

Simplifying Safety Proofs with Forward-Backward Reasoning and Prophecy
di: Frenkel, Eden, et al.
Pubblicazione: (2026)

Products of Recursive Programs for Hypersafety Verification (Extended Version)
di: Cheng, Ruotong, et al.
Pubblicazione: (2025)

Supermartingales for Unique Fixed Points: A Unified Approach to Lower Bound Verification
di: Kura, Satoshi, et al.
Pubblicazione: (2025)

Efficient Implementation of an Abstract Domain of Quantified First-Order Formulas
di: Frenkel, Eden, et al.
Pubblicazione: (2024)

Axe 'Em: Eliminating Spurious States with Induction Axioms
di: Elad, Neta, et al.
Pubblicazione: (2024)

Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions
di: Elad, Neta, et al.
Pubblicazione: (2025)

Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic (Extended Version)
di: Haselwarter, Philipp G., et al.
Pubblicazione: (2026)

JAX Autodiff from a Linear Logic Perspective (Extended Version)
di: Giusti, Giulia, et al.
Pubblicazione: (2025)

Contextual Refinement of Higher-Order Concurrent Probabilistic Programs (Extended Version)
di: Li, Kwing Hei, et al.
Pubblicazione: (2025)

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

Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs (Extended Version)
di: Li, Kwing Hei, et al.
Pubblicazione: (2025)

Lagrangian-Based Duality for Quantified SMT Algorithms - Artifact
di: Bocevska, Ivana, et al.
Pubblicazione: (2026)

Ordered Adjoint Logic (Extended Version)
di: Roshal, Sophia, et al.
Pubblicazione: (2026)

Adjoint Natural Deduction (Extended Version)
di: Jang, Junyoung, et al.
Pubblicazione: (2024)

Hybrid Intersection Types for PCF (Extended Version)
di: Barenbaum, Pablo, et al.
Pubblicazione: (2024)

An Abstract Domain for Heap Commutativity (Extended Version)
di: Pincus, Jared, et al.
Pubblicazione: (2024)

Monadic Intersection Types, Relationally (Extended Version)
di: Gavazzo, Francesco, et al.
Pubblicazione: (2024)

Compositional Symbolic Execution for Correctness and Incorrectness Reasoning (Extended Version)
di: Lööw, Andreas, et al.
Pubblicazione: (2024)

Mechanised Hypersafety Proofs about Structured Data: Extended Version
di: Gladshtein, Vladimir, et al.
Pubblicazione: (2024)

Rely-Guarantee Reasoning for Causally Consistent Shared Memory (Extended Version)
di: Lahav, Ori, et al.
Pubblicazione: (2023)

Structural Temporal Logic for Mechanized Program Verification
di: Ioannidis, Eleftherios, et al.
Pubblicazione: (2024)

FO-Complete Program Verification for Heap Logics
di: Murali, Adithya, et al.
Pubblicazione: (2026)

Implicit Rankings for Verifying Liveness Properties in First-Order Logic
di: Lotan, Raz, et al.
Pubblicazione: (2024)

Functional Array Programming in an Extended Pi-Calculus
di: Hüttel, Hans, et al.
Pubblicazione: (2024)

Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type System
di: Kura, Satoshi, et al.
Pubblicazione: (2024)

Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back
di: Batz, Kevin, et al.
Pubblicazione: (2025)

Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs
di: Chatterjee, Krishnendu, et al.
Pubblicazione: (2024)

A Hierarchy of Supermartingales for $ω$-Regular Verification
di: Kura, Satoshi, et al.
Pubblicazione: (2025)

Qunity: A Unified Language for Quantum and Classical Computing (Extended Version)
di: Voichick, Finn, et al.
Pubblicazione: (2022)

Tunable Automation in Automated Program Verification
di: Bai, Alexander Y., et al.
Pubblicazione: (2025)

Proving Cutoff Bounds for Safety Properties in First-Order Logic
di: Lotan, Raz, et al.
Pubblicazione: (2024)

Hyperproperty Verification as CHC Satisfiability
di: Itzhaky, Shachar, et al.
Pubblicazione: (2023)

Complete the Cycle: Reachability Types with Expressive Cyclic References (Extended Version)
di: Deng, Haotian, et al.
Pubblicazione: (2025)

To bind or not to bind? Discovering Stable Relationships in Object-centric Processes (Extended Version)
di: Seidel, Anjo, et al.
Pubblicazione: (2025)

Automated Software Verification of Hyperliveness
di: Beutner, Raven
Pubblicazione: (2024)

Neural Network Verification is a Programming Language Challenge
di: Cordeiro, Lucas C., et al.
Pubblicazione: (2025)

Handling the Selection Monad (Full Version)
di: Plotkin, Gordon, et al.
Pubblicazione: (2025)

Linearization via Rewriting (Long Version)
di: Lago, Ugo Dal, et al.
Pubblicazione: (2025)