Reasoning about concurrent loops and recursion with rely-guarantee rules

• URL: http://arxiv.org/abs/2512.06242v1
• Date: Sat, 06 Dec 2025 01:57:42 GMT
• Title: Reasoning about concurrent loops and recursion with rely-guarantee rules
• Authors: Ian J. Hayes, Larissa A. Meinicke, Cliff B. Jones,
• Abstract summary: We present general, mechanically verified, refinement for reasoning about programs and loops.<n>We make use of the lattice-guarantee approach to that facilitates reasoning about interference from concurrent threads.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: The objective of this paper is to present general, mechanically verified, refinement rules for reasoning about recursive programs and while loops in the context of concurrency. Unlike many approaches to concurrency, we do not assume that expression evaluation is atomic. We make use of the rely-guarantee approach to concurrency that facilitates reasoning about interference from concurrent threads in a compositional manner. Recursive programs can be defined as fixed points over a lattice of commands and hence we develop laws for reasoning about fixed points. Loops can be defined in terms of fixed points and hence the laws for recursion can be applied to develop laws for loops.

Related papers

• Circular Reasoning: Understanding Self-Reinforcing Loops in Large Reasoning Models [66.11277323593475]
  Circular Reasoning is a self-reinforcing trap where generated content acts as a logical premise for its own recurrence.<n>Mechanistically, we characterize circular reasoning as a state collapse exhibiting distinct boundaries.<n>We reveal that reasoning impasses trigger the loop onset, which subsequently persists as an inescapable cycle driven by a self-reinforcing V-shaped attention mechanism.
  arXiv  Detail & Related papers  (2026-01-09T10:23:55Z)
• To CoT or To Loop? A Formal Comparison Between Chain-of-Thought and Looped Transformers [32.84174396586435]
  Chain-of-Thought (CoT) and Looped Transformers have been shown to empirically improve performance on reasoning tasks.<n>We provide a formal analysis of their respective strengths and limitations.
  arXiv  Detail & Related papers  (2025-05-25T17:49:37Z)
• The nature of loops in programming [37.48416208168878]
  In program semantics and verification, reasoning about loops is complicated by the need to produce two separate mathematical arguments.<n>A single and simple definition is possible, removing this split.<n>To prove the loop correct there is no need to devise an invariant and a variant.<n>It suffices to identify the relation, yielding both partial correctness and termination.
  arXiv  Detail & Related papers  (2025-04-10T20:58:55Z)
• Handling expression evaluation under interference [0.0]
  Hoare-style inference rules for program constructs permit the copying of expressions and tests from program text into logical contexts. The "rely-guarantee" approach does tackle the issue of recording acceptable interference and offers a way to provide safe inference rules.
  arXiv  Detail & Related papers  (2024-09-12T04:16:22Z)
• Invariant Relations: A Bridge from Programs to Equations [1.3342735568824553]
  We propose a method to derive the function of a C-like program, including programs that have loops nested to an arbitrary level. To capture the semantics of loops, we use the concept of invariant relation.
  arXiv  Detail & Related papers  (2023-10-07T04:11:23Z)
• Consistent circuits for indefinite causal order [0.0]
  A number of quantum processes have been proposed which are logically consistent, yet feature a cyclic causal structure. Here we provide a method to construct a process with an exotic causal structure in a way that ensures, and makes clear why, it is consistent. We show how several standard examples of exotic processes, including ones that violate causal inequalities, are among the class of processes that can be generated in this way.
  arXiv  Detail & Related papers  (2022-06-20T23:15:52Z)
• Discovering Non-monotonic Autoregressive Orderings with Variational Inference [67.27561153666211]
  We develop an unsupervised parallelizable learner that discovers high-quality generation orders purely from training data. We implement the encoder as a Transformer with non-causal attention that outputs permutations in one forward pass. Empirical results in language modeling tasks demonstrate that our method is context-aware and discovers orderings that are competitive with or even better than fixed orders.
  arXiv  Detail & Related papers  (2021-10-27T16:08:09Z)
• Discovering Useful Compact Sets of Sequential Rules in a Long Sequence [57.684967309375274]
  COSSU is an algorithm to mine small and meaningful sets of sequential rules. We show that COSSU can successfully retrieve relevant sets of closed sequential rules from a long sequence.
  arXiv  Detail & Related papers  (2021-09-15T18:25:18Z)
• Context-aware and Scale-insensitive Temporal Repetition Counting [60.40438811580856]
  Temporal repetition counting aims to estimate the number of cycles of a given repetitive action. Existing deep learning methods assume repetitive actions are performed in a fixed time-scale, which is invalid for the complex repetitive actions in real life. We propose a context-aware and scale-insensitive framework to tackle the challenges in repetition counting caused by the unknown and diverse cycle-lengths.
  arXiv  Detail & Related papers  (2020-05-18T05:49:48Z)
• Pseudo-Convolutional Policy Gradient for Sequence-to-Sequence Lip-Reading [96.48553941812366]
  Lip-reading aims to infer the speech content from the lip movement sequence. Traditional learning process of seq2seq models suffers from two problems. We propose a novel pseudo-convolutional policy gradient (PCPG) based method to address these two problems.
  arXiv  Detail & Related papers  (2020-03-09T09:12:26Z)
• Consistency of a Recurrent Language Model With Respect to Incomplete Decoding [67.54760086239514]
  We study the issue of receiving infinite-length sequences from a recurrent language model. We propose two remedies which address inconsistency: consistent variants of top-k and nucleus sampling, and a self-terminating recurrent language model.
  arXiv  Detail & Related papers  (2020-02-06T19:56:15Z)
• Retrograde Program Analysis: A Practical Tutorial [51.56484100374058]
  This tutorial condenses a longer exposition to a focused guide with definitions.<n>The aim is practical: short proofs, concrete invariants, and drop-in code and property tests.
  arXiv  Detail & Related papers  (2010-06-13T13:32:37Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.