Please use this identifier to cite or link to this item:
http://hdl.handle.net/10773/27075
Title: | On the generation of equational dynamic logics for weighted imperative programs |
Author: | Gomes, Leandro Madeira, Alexandre Jain, Manisha Barbosa, Luis S. |
Keywords: | Dynamic logic Multi-valued logics Programs verification Formal methods |
Issue Date: | 2019 |
Publisher: | Springer |
Abstract: | 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 structure specifying a notion of ‘weight’ assigned to programs. The paper introduces also a notion of bisimilarity on models of the generated logics, which is shown to entail modal equivalence with respect to the latter. |
Peer review: | yes |
URI: | http://hdl.handle.net/10773/27075 |
DOI: | 10.1007/978-3-030-32409-4_10 |
ISBN: | 978-3-030-32408-7 |
Publisher Version: | https://link.springer.com/chapter/10.1007%2F978-3-030-32409-4_10 |
Appears in Collections: | CIDMA - Capítulo de livro AGG - Capítulo de livro |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
paper_30.pdf | 353.56 kB | Adobe PDF | View/Open |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.