Buchumschlag

An example of goal-directed, calculational proof

Fuente: arXiv

Gespeichert in:

Bibliographische Detailangaben
Hauptverfasser:	Backhouse, Roland, Guttmann, Walter, Winter, Michael
Format:	Preprint
Veröffentlicht:	2023
Schlagworte:	Logic in Computer Science D.1; F.3.1
Online-Zugang:	Acceder al recurso
Tags:	Tag hinzufügen Keine Tags, Fügen Sie den ersten Tag hinzu!

Ähnliche Einträge

Relation-Algebraic Verification of Disjoint-Set Forests
von: Guttmann, Walter
Veröffentlicht: (2023)

The Index and Core of a Relation. With Applications to the Axiomatics of Relation Algebra
von: Backhouse, Roland, et al.
Veröffentlicht: (2023)

Diagonals and Block-Ordered Relations
von: Backhouse, Roland, et al.
Veröffentlicht: (2024)

The Thins Ordering on Relations
von: Voermans, Ed, et al.
Veröffentlicht: (2024)

Reasoning about distributive laws in a concurrent refinement algebra
von: Meinicke, Larissa A., et al.
Veröffentlicht: (2024)

Restructuring a concurrent refinement algebra
von: Hayes, Ian J., et al.
Veröffentlicht: (2024)

Generically Automating Separation Logic by Functors, Homomorphisms and Modules
von: Xu, Qiyuan, et al.
Veröffentlicht: (2024)

Unified Fairness for Weak Memory Verification
von: Abdulla, Parosh Aziz, et al.
Veröffentlicht: (2023)

Well-Scoped Locally Nameless Representation of Syntax
von: Pitts, Andrew M.
Veröffentlicht: (2026)

Separation Logic of Generic Resources via Sheafeology
von: van Starkenburg, Berend, et al.
Veröffentlicht: (2025)

Simple Types for Polymorphic Functions
von: Jay, Barry, et al.
Veröffentlicht: (2026)

Bounded Modal Logic
von: Murase, Yuito, et al.
Veröffentlicht: (2026)

Explicit Weakening
von: Wadler, Philip
Veröffentlicht: (2024)

Verification of E-Voting Algorithms in Dafny
von: Büttner, Robert, et al.
Veröffentlicht: (2025)

Complementing an imperative process algebra with a rely/guarantee logic
von: Middelburg, C. A.
Veröffentlicht: (2025)

Probabilistic imperative process algebra
von: Middelburg, C. A.
Veröffentlicht: (2026)

Reasoning about expression evaluation under interference
von: Hayes, Ian J., et al.
Veröffentlicht: (2024)

Data reification in a concurrent rely-guarantee algebra
von: Meinicke, Larissa A., et al.
Veröffentlicht: (2024)

Propositional Dynamic Logic has Craig Interpolation: a tableau-based proof
von: Borzechowski, Manfred, et al.
Veröffentlicht: (2025)

Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration (Extended Version)
von: Sextl, Florian, et al.
Veröffentlicht: (2023)

SMT-based Symbolic Model-Checking for Operator Precedence Languages
von: Chiari, Michele, et al.
Veröffentlicht: (2024)

Sound and Complete Invariant-Based Heap Encodings (Technical Report)
von: Esen, Zafer, et al.
Veröffentlicht: (2025)

Semi-Automated Modular Formal Verification of Critical Software: Liveness and Completeness Thresholds
von: Reinhard, Tobias
Veröffentlicht: (2024)

Automatic Function Annotations for Hoare Logic
von: Matichuk, Danielle
Veröffentlicht: (2012)

Automating the Derivation of Unification Algorithms: A Case Study in Deductive Program Synthesis
von: Waldinger, Richard
Veröffentlicht: (2025)

Refactoring-as-Propositions: Proved Refactoring of Hybrid Systems via Proved Refinements
von: Prebet, Enguerrand, et al.
Veröffentlicht: (2026)

Uniform Substitution for Differential Refinement Logic
von: Prebet, Enguerrand, et al.
Veröffentlicht: (2024)

Verified VCG and Verified Compiler for Dafny
von: Nezamabadi, Daniel, et al.
Veröffentlicht: (2025)

A Graded Modal Type Theory for Pulse Schedules
von: Adams, Robin, et al.
Veröffentlicht: (2025)

Extending the Quantitative Pattern-Matching Paradigm
von: Alves, Sandra, et al.
Veröffentlicht: (2024)

Genericity Through Stratification
von: Arrial, Victor, et al.
Veröffentlicht: (2024)

AdapTT: Functoriality for Dependent Type Casts
von: Adjedj, Arthur, et al.
Veröffentlicht: (2025)

Monitoring Hyperproperties over Observed and Constructed Traces
von: Chalupa, Marek, et al.
Veröffentlicht: (2025)

Constrained LTL Specification Learning from Examples
von: Zhang, Changjian, et al.
Veröffentlicht: (2024)

Definitional Functoriality for Dependent (Sub)Types -- Extended version
von: Laurent, Théo, et al.
Veröffentlicht: (2023)

Sufficient Incorrectness Logic: SIL and Separation SIL
von: Ascari, Flavio, et al.
Veröffentlicht: (2023)

Just Verification of Mutual Exclusion Algorithms with (Non-)Blocking and (Non-)Atomic Registers
von: van Glabbeek, Rob, et al.
Veröffentlicht: (2026)

Gradual C0: Symbolic Execution for Gradual Verification
von: DiVincenzo, Jenna, et al.
Veröffentlicht: (2022)

A Complete Axiomatization of Branching Bisimilarity for a Simple Process Language with Probabilistic Choice
von: van Glabbeek, Rob, et al.
Veröffentlicht: (2025)

Centralized vs Decentralized Monitors for Hyperproperties
von: Aceto, Luca, et al.
Veröffentlicht: (2024)