A nesting-preserving transformation of SIMP programs into logically constrained term rewrite systems

DOI10.1016/J.JLAMP.2025.101045MaRDI QIDQ7009391zbMATH OpenFDO

Authors Naoki Nishida, Misaki Kojima, Ayuka Matsumi

Publication date 20 March 2025

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/J.JLAMP.2025.101045

zbMATH Keywords

constrained rewritingprogram transformationprogram verificationtree homomorphism

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Grammars and rewriting systems (68Q42)

Cites work

• A coinductive approach to proving reachability properties in logically constrained term rewriting systems
• A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs
• All-path reachability logic
• All-path reachability logic
• An overview of the K semantic framework
• Automatic synthesis of logical models for order-sorted first-order theories
• Completion for logically constrained rewriting
• Constrained term rewriting tooL
• Decision procedures. An algorithmic point of view
• Dynamic dependency pairs for algebraic functional systems
• scientific article; zbMATH DE number 1729952 (Why is no real title available?)
• scientific article; zbMATH DE number 1487842 (Why is no real title available?)
• Logic for Programming, Artificial Intelligence, and Reasoning
• Loop detection by logically constrained term rewriting
• Mechanizing and improving dependency pairs
• On proving termination of constrained term rewrite systems by eliminating edges from dependency graphs
• 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
• Soundness of unravelings for conditional term rewriting systems via ultra-properties related to linearity
• Term Rewriting with Logical Constraints
• Termination and complexity analysis for programs with bitvector arithmetic by symbolic execution
• Termination Competition (termCOMP 2015)
• Termination of term rewriting using dependency pairs
• Transforming concurrent programs with semaphores into logically constrained term rewrite systems
• Tuple interpretations for termination of term rewriting
• Verifying procedural programs via constrained rewriting induction

Cited in

(1)

• Difference of constrained patterns in logically constrained term rewrite systems

This page was built for publication: A nesting-preserving transformation of SIMP programs 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 Q7009391)