Towards a Rewriting-Logic Semantics of P





Publicado en

Actas de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023)

Licencia Creative Commons


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.


Acerca de Durán, Francisco

Palabras clave

P Language, Rewriting Logic, Maude, Model Checking, Reachability Analysis
Página completa del ítem
Notificar un error en este artículo
Mostrar cita
Mostrar cita en BibTeX
Descargar cita en BibTeX