Please use this identifier to cite or link to this item:
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
DOI: 10.1007/978-3-030-32409-4_10
ISBN: 978-3-030-32408-7
Publisher Version:
Appears in Collections:CIDMA - Capítulo de livro
AGG - Capítulo de livro

Files in This Item:
File Description SizeFormat 
paper_30.pdf353.56 kBAdobe PDFView/Open

Formato BibTex MendeleyEndnote Degois 

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.