Transforming concurrent programs with semaphores into logically constrained term rewrite systems
From MaRDI portal
Recommendations
Cites work
- A coinductive approach to proving reachability properties in logically constrained term rewriting systems
- All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
- An overview of the K semantic framework
- Automatic constrained rewriting induction towards verifying procedural programs
- Completion for logically constrained rewriting
- Conditional rewriting logic as a unified model of concurrency
- Decision procedures. An algorithmic point of view
- Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures
- Ensuring the quasi-termination of needed narrowing computations
- Formalizing the LLVM intermediate representation for verified program transformations
- scientific article; zbMATH DE number 1729952 (Why is no real title available?)
- scientific article; zbMATH DE number 7189131 (Why is no real title available?)
- Loop detection by logically constrained term rewriting
- One-path reachability logic
- Operationally-based program equivalence proofs using LCTRSs
- Programming languages and operational semantics. A concise overview
- Reducing non-occurrence of specified runtime errors to all-path reachability problems of constrained rewriting
- Rewriting Induction + Linear Arithmetic = Decision Procedure
- Rewriting logic as a semantic framework for concurrency: a progress report
- Term rewriting induction
- Term Rewriting with Logical Constraints
- Termination of rewriting
- The Maude strategy language
- 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. Procee
- Verifying procedural programs via constrained rewriting induction
Cited in
(3)- Difference of constrained patterns in logically constrained term rewrite systems
- Transforming imperative programs into bisimilar logically constrained term rewrite systems via injective functions from configurations to terms
- A nesting-preserving transformation of SIMP programs into logically constrained term rewrite systems
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)
