Transforming concurrent programs with semaphores into logically constrained term rewrite systems
type: Item
instance of: scholarly article
title: Transforming concurrent programs with semaphores into logically constrained term rewrite systems
author: Misaki Kojima
author: Naoki Nishida
author: Yutaka Matsubara
published in: Journal of Logical and Algebraic Methods in Programming
publication date: 2025-01-27T00:00:00Z
Mathematics Subject Classification ID: 68-XX
zbMATH DE Number: 7975263
zbMATH Keywords: constrained rewriting
zbMATH Keywords: program transformation
zbMATH Keywords: program verification
zbMATH Keywords: imperative program
zbMATH Keywords: concurrency
MaRDI profile type: MaRDI publication profile
cites work: Term Rewriting with Logical Constraints
cites work: Verifying Procedural Programs via Constrained Rewriting Induction
cites work: Q4993362
cites work: A coinductive approach to proving reachability properties in logically constrained term rewriting systems
cites work: Loop detection by logically constrained term rewriting
cites work: Reducing non-occurrence of specified runtime errors to all-path reachability problems of constrained rewriting
cites work: Operationally-based program equivalence proofs using LCTRSs
cites work: Term rewriting induction
cites work: Rewriting Induction + Linear Arithmetic = Decision Procedure
cites work: Ensuring the quasi-termination of needed narrowing computations
cites work: Termination of rewriting
cites work: Q2783416
cites work: Decision procedures. An algorithmic point of view
cites work: Programming languages and operational semantics. A concise overview
cites work: Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures
cites work: Automatic Constrained Rewriting Induction towards Verifying Procedural Programs
cites work: Q2479551
cites work: An overview of the K semantic framework
cites work: Q4960258
cites work: All-Path Reachability Logic
cites work: One-Path Reachability Logic
cites work: Formalizing the LLVM intermediate representation for verified program transformations
cites work: All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
cites work: Conditional rewriting logic as a unified model of concurrency
cites work: Rewriting logic as a semantic framework for concurrency: a progress report
cites work: The Maude strategy language
DOI: 10.1016/J.JLAMP.2024.101033
description: scientific article; zbMATH DE number 7975263