An unresolved issue in SWRL (the Semantic Web Rule Language) is whether the intended semantics of its RDF representation can be described as an extension of the W3C RDF semantics....
This paper is a case study in combining theorem provers. We define a derived rule in HOL-Light, CVC PROVE, which calls CVC Lite and translates the resulting proof object back to HO...
In this paper, we address the issue of the formal verification of real-time systems in the context of a preemptive scheduling policy. We propose an algorithm which computes the st...
Locality is a standard notion of finite model theory. There are two well known flavors of it, based on Hanf's and Gaifman's theorems. Essentially they say that structure...
In this paper, we look at two categorical accounts of computational effects (strong monad as a model of the monadic metalanguage, adjunction as a model of call-bypush-value with s...
Model transformation means converting an input model available at the beginning of the transformation process to an output model. A widely used approach to model transformation us...
In multilevel systems it is important to avoid unwanted indirect information flow from higher levels to lower levels, namely the so called covert channels. Initial studnformation ...
Ruggero Lanotte, Andrea Maggiolo-Schettini, Angelo...
We compare the expressive power of Hoare (i.e., CSP style) and Milner (i.e., CCS style) synchronizations for defining graph transformations in a framework where edges can perform ...
Using graph transformation as a formalism to specify model transformation, termination and confluence of the graph transformation system are often required properties. Only under ...