Cover Image

Data reification in a concurrent rely-guarantee algebra

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Meinicke, Larissa A., Hayes, Ian J., Jones, Cliff B.
Format:	Preprint
Published:	2024
Subjects:	Logic in Computer Science Software Engineering F.3.1; D.1.3
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Reasoning about concurrent loops and recursion with rely-guarantee rules
by: Hayes, Ian J., et al.
Published: (2025)

Reasoning about expression evaluation under interference
by: Hayes, Ian J., et al.
Published: (2024)

Reasoning about distributive laws in a concurrent refinement algebra
by: Meinicke, Larissa A., et al.
Published: (2024)

Restructuring a concurrent refinement algebra
by: Hayes, Ian J., et al.
Published: (2024)

Complementing an imperative process algebra with a rely/guarantee logic
by: Middelburg, C. A.
Published: (2025)

Constrained LTL Specification Learning from Examples
by: Zhang, Changjian, et al.
Published: (2024)

Probabilistic imperative process algebra
by: Middelburg, C. A.
Published: (2026)

Quantifying Confidence in Assurance 2.0 Arguments
by: Bloomfield, Robin, et al.
Published: (2026)

Monitoring Unmanned Aircraft: Specification, Integration, and Lessons-learned
by: Baumeister, Jan, et al.
Published: (2024)

Towards Bug-Free Distributed Go Programs
by: Koo, Zhengqun
Published: (2025)

Dormancy-aware timed branching bisimilarity, with an application to communication protocol analysis
by: Middelburg, C. A.
Published: (2021)

Formal Verification of Imperative First-Class Functions in Move
by: Grieskamp, Wolfgang, et al.
Published: (2026)

Imperative process algebra and models of computation
by: Middelburg, C. A.
Published: (2022)

Separation Logic of Generic Resources via Sheafeology
by: van Starkenburg, Berend, et al.
Published: (2025)

Software Verification with CPAchecker 3.0: Tutorial and User Guide (Extended Version)
by: Baier, Daniel, et al.
Published: (2024)

MoXIchecker: An Extensible Model Checker for MoXI
by: Ates, Salih, et al.
Published: (2024)

Unified Fairness for Weak Memory Verification
by: Abdulla, Parosh Aziz, et al.
Published: (2023)

Quantitative Assurance and Synthesis of Controllers from Activity Diagrams
by: Ye, Kangfeng, et al.
Published: (2024)

Generically Automating Separation Logic by Functors, Homomorphisms and Modules
by: Xu, Qiyuan, et al.
Published: (2024)

An example of goal-directed, calculational proof
by: Backhouse, Roland, et al.
Published: (2023)

Explicit Weakening
by: Wadler, Philip
Published: (2024)

Simple Types for Polymorphic Functions
by: Jay, Barry, et al.
Published: (2026)

Bounded Modal Logic
by: Murase, Yuito, et al.
Published: (2026)

Do Unit Proofs Work? An Empirical Study of Compositional Bounded Model Checking for Memory Safety Verification
by: Amusuo, Paschal C., et al.
Published: (2025)

QuickCheck for VDM
by: Battle, Nick, et al.
Published: (2024)

A Unit Proofing Framework for Code-level Verification: A Research Agenda
by: Amusuo, Paschal C., et al.
Published: (2024)

Well-Scoped Locally Nameless Representation of Syntax
by: Pitts, Andrew M.
Published: (2026)

A Gentle Overview of Asynchronous Session-based Concurrency: Deadlock Freedom by Typing
by: Heuvel, Bas van den, et al.
Published: (2024)

Position: Vibe Coding Needs Vibe Reasoning: Improving Vibe Coding with Formal Verification
by: Mitchell, Jacqueline, et al.
Published: (2025)

Verified VCG and Verified Compiler for Dafny
by: Nezamabadi, Daniel, et al.
Published: (2025)

A Graded Modal Type Theory for Pulse Schedules
by: Adams, Robin, et al.
Published: (2025)

Converting BPMN Diagrams to Privacy Calculus
by: Pitsiladis, Georgios V., et al.
Published: (2024)

The concept of class invariant in object-oriented programming
by: Meyer, Bertrand, et al.
Published: (2021)

Formal Verification of COO to CSR Sparse Matrix Conversion (Invited Paper)
by: Appel, Andrew W.
Published: (2025)

Space-time process algebra with asynchronous communication
by: Bergstra, J. A., et al.
Published: (2024)

Definitional Functoriality for Dependent (Sub)Types -- Extended version
by: Laurent, Théo, et al.
Published: (2023)

Monitoring Hyperproperties over Observed and Constructed Traces
by: Chalupa, Marek, et al.
Published: (2025)

What does it take to certify a conversion checker?
by: Lennon-Bertrand, Meven
Published: (2025)

Verification of E-Voting Algorithms in Dafny
by: Büttner, Robert, et al.
Published: (2025)

Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration (Extended Version)
by: Sextl, Florian, et al.
Published: (2023)