A rewriting logic semantics for the analysis of \textsf{P} programs

DOI10.1016/J.JLAMP.2025.101048MaRDI QIDQ7009386zbMATH OpenFDO

Authors Francisco Durán, Carlos Alonso Herrera Ramírez, Camilo Rocha, Nicolás Pozas

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.101048

zbMATH Keywords

equational abstractionLTL model checkingMaudemodel checkingreachability analysisstatistical model checking

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Grammars and rewriting systems (68Q42) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Cites work

• Algebraic Methodology and Software Technology
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• An efficient canonical narrowing implementation with irreducibility and SMT constraints for generic symbolic protocol analysis
• Automated Reasoning
• Computer Aided Verification
• Computer Aided Verification
• Conditional rewriting logic as a unified model of concurrency
• Equational abstractions
• Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description)
• PMaude: rewrite-based specification language for probabilistic object systems
• Predicate abstraction of rewrite theories
• Programming and symbolic computation in Maude
• QMaude: quantitative specification and verification in rewriting logic
• Rewriting logic semantics of a plan execution language
• Rewriting modulo SMT and open system analysis
• Specification and proof in membership equational logic
• State Space Reduction of Rewrite Theories Using Invisible Transitions
• Strategies, model checking and branching-time properties in Maude
• The Maude LTL model checker
• The rewriting logic semantics project
• The rewriting logic semantics project: a progress report

Cited in

(1)

• Preface to selected papers from 22nd workshop on programming and languages (PROLE 2023)

This page was built for publication: A rewriting logic semantics for the analysis of \textsf{P} programs

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