In object-oriented programming, reentrant method invocations and shared references make it difficult to achieve adequate encapsulation for sound modular reasoning. This tutorial p...
Abstract. The Verifying Compiler (VC) project proposals suggest that mainstream software developers are its targeted end-users. Like other software engineering efforts, the VC proj...
Abstract. In this paper we consider two performance modelling techniques from the perspectives of model construction, generation of an underlying continuous time Markov process, an...
Abstract. We report on a case study in applying different formal methods to model and verify an architecture for administrating digital signatures. The architecture comprises seve...
David A. Basin, Hironobu Kuruma, Kunihiko Miyazaki...
Abstract. We develop a model of Parametric Probabilistic Transition Systems, where probabilities associated with transitions may be parameters. We show how to find instances of th...
Ruggero Lanotte, Andrea Maggiolo-Schettini, Angelo...
Individual components in an inter-operating system require assurance from other components both of appropriate functionality and of suitable responsiveness. We have developed prope...