Abstract. We develop an algebraic modal logic that combines epistemic and dynamic modalities with a view to modelling information acquisition (learning) by automated agents in a ch...
Fusion is an indispensable tool in the arsenal of techniques for program derivation. Less well-known, but equally valuable is type fusion, which states conditions for fusing an app...
mu-term is a tool which can be used to verify a number of termination properties of (variants of) Term Rewriting Systems (TRSs): termination of rewriting, termination of innermost ...
Maude modules can be understood as models that can be formally analyzed and verified with respect to different properties expressing various formal requirements. However, Maude lac...
Abstract. We present a declarative debugger for Maude specifications that allows to debug wrong answers (a wrong result is obtained) and missing answers (a correct but incomplete r...
Abstract. This paper introduces matching logic, a novel framework for defining axiomatic semantics for programming languages, inspired from operational semantics. Matching logic sp...