Cover Image

Reasoning about concurrent loops and recursion with rely-guarantee rules

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Hayes, Ian J., Meinicke, Larissa A., Jones, Cliff B.
Format:	Preprint
Published:	2025
Subjects:	Logic in Computer Science Programming Languages 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

Data reification in a concurrent rely-guarantee algebra
by: Meinicke, Larissa A., et al.
Published: (2024)

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)

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)

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

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

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

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

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

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

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

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

Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification
by: Beyer, Dirk, et al.
Published: (2022)

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

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

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

Modelling Distributed Applications with Mixed-Choice Stateful Typestates
by: Parrinha, Francisco, et al.
Published: (2026)

A Calculus of Inheritance
by: Yang, Bo
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)

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

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

Have a thing? Reasoning around recursion with dynamic typing in grounded arithmetic
by: Bobrow, Elliot, et al.
Published: (2025)

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

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

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

Genericity Through Stratification
by: Arrial, Victor, et al.
Published: (2024)

AdapTT: Functoriality for Dependent Type Casts
by: Adjedj, Arthur, et al.
Published: (2025)

On Modular Termination Proofs of General Logic Programs
by: Bossi, Annalisa, et al.
Published: (2000)

Sequence-Based Abstract Interpretation of Prolog
by: Charlier, Baudouin Le, et al.
Published: (2000)

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

Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agents
by: Lahiri, Shuvendu K.
Published: (2026)

Bisimilarity and Simulatability of Processes Parameterized by Join Interactions
by: Grabmayer, Clemens, et al.
Published: (2025)

Multisets and Distributions
by: Kozen, Dexter, et al.
Published: (2023)

HpC: A Calculus for Hybrid and Mobile Systems -- Full Version
by: Xu, Xiong, et al.
Published: (2025)