We study the proof theory and algorithms for orthologic, a logical system based on ortholattices, which have shown practical relevance in simplification and normalization of verification conditions. Ortholattices weaken Boolean algebras while having polyno ...
RDF and SPARQL are established standards for data interchange and querying on the Web. While they have been shown to be useful and applicable in many scenarios, they are not sufficiently adequate for dealing with streams of data and their intrinsic continu ...
Cryptographic protocols are an essential component of network communications. Despite their relatively small size compared to other distributed algorithms, they are known to be error-prone. This is due to the obligation to behave robustly in the context of ...
In this dissertation we investigate how Business/IT alignment in enterprise models can be enhanced by using a software engineering stepwise refinement paradigm. To have an IT system that supports an enterprise and meets the enterprise business needs, manag ...
This work concentrates on improving the robustness of constraint solvers by increasing the propagation strength of constraint models in a declarative and automatic manner. Our objective is to efficiently identify and remove shavable values during search. A ...
Springer-Verlag New York, Ms Ingrid Cunningham, 175 Fifth Ave, New York, Ny 10010 Usa2008
SEAM is an enterprise architecture method that defines a visual language for modeling. Our goal is to provide formal semantics for SEAM. Model simulation, model comparison, and refinement verification are practical benefits we expect from this formalizatio ...
Protocol narrations are a widely-used informal means to describe, in an idealistic manner, the functioning of cryptographic protocols as a single intended sequence of cryptographic message exchanges among the protocol’s participants. Protocol narrations ha ...
This paper presents a semantic foundation of temporal conceptual models used to design temporal information systems. We consider a modelling language able to express both timestamping and evolution constraints. We conduct a deeper investigation of evolutio ...
SCALA is an attractive programming language because it is both very expressive and statically strongly typed. This marriage against nature comes at the price of a certain complexity in the language constructs and the static analysis. This complexity makes ...
Protocol narrations are an informal means to describe, in an idealistic manner, the functioning of cryptographic protocols as a single intended sequence of cryptographic message exchanges among the protocol's participants. Protocol narrations have also bee ...
We present a method of formal description of the action semantics in smart objects. Smart objects were primarily used for behavioral animation in the past. We demonstrate, how a formally described semantics can be used for action planning purposes by intel ...