Rewriting logic provides a powerful, flexible mechanism for language definition and analysis. This flexibility in design can lead to problems during analysis, as different desi...
In this paper we present a formalization of Abadi’s and Cardelli’s theory of objects in the interactive theorem prover Isabelle/HOL. Our motivation is to build a mechanized HOL...
The Pict programming language is an implementation of the π-calculus in which executions of π-calculus terms are specified via an abstract machine. An important property of any ...
Abstract. This paper gives an overview of the KeY approach and highlights the main features of the KeY system. KeY is an approach (and a system) for the deductive verification of ...
The success of distributed event-based infrastructures such as SIENA and Elvin is partially due to their ease of use. Even novice users of these infrastructures not versed in distr...
This paper describes the application of Real-Time Maude to the formal specification, simulation, and further formal analysis of the sophisticated state-of-the-art OGDC wireless se...
We present a novel approach, based on probabilistic formal methods, to developing cross-layer resource optimization policies for resource limited distributed systems. One objective...
Minyoung Kim, Mark-Oliver Stehr, Carolyn L. Talcot...
Abstract. A session type is an abstraction of a sequence of heterogeneous values sent over one channel between two communicating processes. Session types have been introduced to gu...
Mario Coppo, Mariangiola Dezani-Ciancaglini, Nobuk...
We present the first tool that offers dynamic verification of extended traints on UML models. It translates a UML model into an Abstract State (ASM) which is transformed by an AS...