Reducing non-occurrence of specified runtime errors to all-path reachability problems of constrained rewriting

DOI10.1016/j.jlamp.2023.100903MaRDI QIDQ6052950

Misaki Kojima, Naoki Nishida

Publication date: 25 September 2023

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

zbMATH Keywords

program transformationconstrained rewritingruntime-error verification

Mathematics Subject Classification ID

Computer science (68-XX)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Equational approximations for tree automata completion
• An overview of the K semantic framework
• Myths about the mutual exclusion problem
• Loop detection by logically constrained term rewriting
• A coinductive approach to proving reachability properties in logically constrained term rewriting systems
• Automatic Constrained Rewriting Induction towards Verifying Procedural Programs
• Term Rewriting with Logical Constraints
• Abstract Logical Model Checking of Infinite-State Systems Using Narrowing
• Reachability Analysis of Term Rewriting Systems with Timbuk
• Decidable approximations of term rewriting systems
• All-Path Reachability Logic
• Verifying Procedural Programs via Constrained Rewriting Induction
• Automated Reasoning with Analytic Tableaux and Related Methods

This page was built for publication: Reducing non-occurrence of specified runtime errors to all-path reachability problems of constrained rewriting