Please use this identifier to cite or link to this item:
|Title:||On the generation of equational dynamic logics for weighted imperative programs|
Barbosa, Luis S.
|Abstract:||Dynamic logic is a powerful framework for reasoning about imperative programs. This paper extends previous work  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.|
|Appears in Collections:||CIDMA - Capítulo de livro|
AGG - Capítulo de livro
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.