Transforming concurrent programs with semaphores into logically constrained term rewrite systems

Cites Work

Title not available (Why is that?)
Title not available (Why is that?)
Title not available (Why is that?)
All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
Formalizing the LLVM intermediate representation for verified program transformations
An overview of the K semantic framework
Termination of rewriting
Conditional rewriting logic as a unified model of concurrency
Automatic Constrained Rewriting Induction towards Verifying Procedural Programs
Term Rewriting with Logical Constraints
Rewriting Induction + Linear Arithmetic = Decision Procedure
Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures
Rewriting logic as a semantic framework for concurrency: a progress report
Programming languages and operational semantics. A concise overview
Tools and algorithms for the construction and analysis of systems. 14th international conference, TACAS 2008, held as part of the joint European conferences on theory and practice of software, ETAPS 2008, Budapest, Hungary, March 29--April 6, 2008. Proceedings
All-Path Reachability Logic
One-Path Reachability Logic
Term rewriting induction
Decision procedures. An algorithmic point of view
A coinductive approach to proving reachability properties in logically constrained term rewriting systems
Verifying Procedural Programs via Constrained Rewriting Induction
Ensuring the quasi-termination of needed narrowing computations
Loop detection by logically constrained term rewriting
Operationally-based program equivalence proofs using LCTRSs
Reducing non-occurrence of specified runtime errors to all-path reachability problems of constrained rewriting
The Maude strategy language

This page was built for publication: Transforming concurrent programs with semaphores into logically constrained term rewrite systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6671788)