Rewriting Logic

URI permanente para esta colección:

https://hdl.handle.net/11705/PROLE/2023/RL
Artículos en la categoría Rewriting Logic publicados en las Actas de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023).
Notificar un error en esta colección

Examinar

Envíos recientes

Mostrando 1 - 3 de 3
  • Miniatura
    Resumen
    Canonical Narrowing for Variant-Based Conditional Rewrite Theories
    López Rueda, Raúl; Escobar, Santiago. Actas de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023), 2023-09-12.
    23rd International Conference on Formal Engineering Methods (ICFEM 2022). Madrid, Spain: Springer. Maude currently supports many symbolic reasoning features such as order-sorted equational unification and order-sorted narrowingbased symbolic reachability analysis. There have been many advances and new features added to improve narrowing in Maude but only at a theoretical level. In this paper, we provide a very elegant, transparent, and extremely pragmatic approach for conditional rewrite theories where the conditions are just equalities solved by equational unification. We show how two conditional theories, never executed before, are now executable with very good performance.We also show how real execution works better than the manually transformed version.
  • Miniatura
    Resumen
    QMaude: quantitative specification and verification in rewriting logic
    Rubio, Rubén; Martí-Oliet, Narciso; Pita, Isabel; Verdejo, Alberto. Actas de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023), 2023-09-12.
    In formal verification, qualitative and quantitative aspects are both relevant, and high-level formalisms are convenient to naturally specify the systems under study and their properties. In this paper, we present a framework for describing probabilistic models on top of nondeterministic specifications in the highly-expressive language Maude, based on rewriting logic. Quantitative properties can be checked and calculated on them using both probabilistic and statistical methods with external tools like PRISM, Storm, MultiVeSta, and custom implementations as backends. At the same time, the underlying nondeterministic system can be verified using the qualitative model-checking and deductive tools already available in Maude.
  • Miniatura
    Artículo
    Towards a Rewriting-Logic Semantics of P
    Durán, Francisco; Pozas García, Nicolás; Ramírez, Carlos; Rocha, Camilo. Actas de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023), 2023-09-12.
    P is a programming language based on state machines, suited for the definition of asynchronous event-driven open systems. The language was designed with verification in mind and it is bundled with back-end analysis engines for, e.g., bounded model checking. With the aim of extending such verification capabilities, a semantics of P in rewriting logic has been developed. Given this formal semantics, developed using the rewriting-logic language Maude, the Maude Formal Environment (MFE) can now be used to carry on different types of analyses on P programs. These capabilities are illustrated by carrying on reachability analysis and model checking of P programs.