On the generation of equational dynamic logics for weighted imperative programs

Dynamic logic is a powerful framework for reasoning about imperative programs. This paper extends previous work [9] on the systematic generation of dynamic logics from the propositional to the equational case, to capture ‘full-fledged’ imperative programs. The generation process is parametric on a s...

Full description

Bibliographic Details
Main Author: Gomes, Leandro (author)
Other Authors: Madeira, Alexandre (author), Jain, Manisha (author), Barbosa, Luis S. (author)
Format: bookPart
Language:eng
Published: 2019
Subjects:
Online Access:http://hdl.handle.net/10773/27075
Country:Portugal
Oai:oai:ria.ua.pt:10773/27075