Copertina

Coinductive Proofs for Temporal Hyperliveness

Fuente: arXiv

Salvato in:

Dettagli Bibliografici
Autori principali:	Correnson, Arthur, Finkbeiner, Bernd
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 Intermediate Program Representation for Optimizing Stream-Based Languages
di: Baumeister, Jan, et al.
Pubblicazione: (2025)

A Deductive System for Contract Satisfaction Proofs
di: Correnson, Arthur, et al.
Pubblicazione: (2026)

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

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

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

Symmetric Proofs of Parameterized Programs
di: Cheng, Ruotong, et al.
Pubblicazione: (2026)

More Church-Rosser Proofs in BELUGA
di: Momigliano, Alberto, et al.
Pubblicazione: (2024)

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

Pleasant Imperative Program Proofs with GallinaC
di: Fort, Frédéric, et al.
Pubblicazione: (2025)

Zippy -- Generic White-Box Proof Search with Zippers
di: Kappelmann, Kevin
Pubblicazione: (2025)

Formalising Inductive and Coinductive Containers
di: Damato, Stefania, et al.
Pubblicazione: (2024)

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

Proof systems for partial incorrectness logic (partial reverse Hoare logic)
di: Oda, Yukihiro
Pubblicazione: (2025)

A Mixed Linear and Graded Logic: Proofs, Terms, and Models (with appendices)
di: Vollmer, Victoria, et al.
Pubblicazione: (2024)

Kleene algebra with commutativity conditions is undecidable
di: de Amorim, Arthur Azevedo, et al.
Pubblicazione: (2024)

Closure and Complexity of Temporal Causality
di: Carelli, Mishel, et al.
Pubblicazione: (2025)

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)

Logics and Algorithms for Hyperproperties
di: Finkbeiner, Bernd
Pubblicazione: (2025)

Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge
di: Kolesar, John, et al.
Pubblicazione: (2025)

A Coinductive Reformulation of Milner's Proof System for Regular Expressions Modulo Bisimilarity
di: Grabmayer, Clemens
Pubblicazione: (2022)

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

revTPL: The Reversible Temporal Process Language
di: Bocchi, Laura, et al.
Pubblicazione: (2022)

Finding $\forall\exists$ Hyperbugs using Symbolic Execution
di: Correnson, Arthur, et al.
Pubblicazione: (2025)

Pacing Types: Safe Monitoring of Asynchronous Streams
di: Kohn, Florian, et al.
Pubblicazione: (2025)

Pacing Types for Asynchronous Stream Equations
di: Kohn, Florian, et al.
Pubblicazione: (2026)

Domain Reasoning in TopKAT
di: Zhang, Cheng, et al.
Pubblicazione: (2024)

Complexity of Model Checking Second-Order Hyperproperties on Finite Structures
di: Finkbeiner, Bernd, et al.
Pubblicazione: (2026)

Counterfactual Explanations for MITL Violations
di: Finkbeiner, Bernd, et al.
Pubblicazione: (2024)

An Introduction to Razborov's Flag Algebra as a Proof System for Extremal Graph Theory
di: Jeong, Gyeongwon, et al.
Pubblicazione: (2026)

Non-Deterministic Planning for Hyperproperty Verification
di: Beutner, Raven, et al.
Pubblicazione: (2024)

Synthesis of Temporal Causality
di: Finkbeiner, Bernd, et al.
Pubblicazione: (2024)

A Proof-Producing Compiler for Blockchain Applications
di: Avigad, Jeremy, et al.
Pubblicazione: (2025)

Totality for Mixed Inductive and Coinductive Types
di: Hyvernat, Pierre
Pubblicazione: (2019)

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

Towards a Certified Proof Checker for Deep Neural Network Verification
di: Desmartin, Remi, et al.
Pubblicazione: (2023)

A Certified Proof Checker for Deep Neural Network Verification in Imandra
di: Desmartin, Remi, et al.
Pubblicazione: (2024)

Compression for Coinductive Infinitary Rewriting: A Generic Approach, with Applications to Cut-Elimination for Non-Wellfounded Proofs
di: Cerda, Rémy, et al.
Pubblicazione: (2025)

MiniF2F in Rocq: Automatic Translation Between Proof Assistants -- A Case Study
di: Viennot, Jules, et al.
Pubblicazione: (2025)

On Alternating-Time Temporal Logic, Hyperproperties, and Strategy Sharing
di: Beutner, Raven, et al.
Pubblicazione: (2023)

Explainability Requirements as Hyperproperties
di: Finkbeiner, Bernd, et al.
Pubblicazione: (2025)