Sciweavers

FMCO
2007
Springer
124views Formal Methods» more  FMCO 2007»
13 years 8 months ago
Certification Using the Mobius Base Logic
This paper describes a core component of Mobius' Trusted Code Base, the Mobius base logic. This program logic facilitates the transmission of certificates that are generated u...
Lennart Beringer, Martin Hofmann, Mariela Pavlova
FMCO
2007
Springer
196views Formal Methods» more  FMCO 2007»
13 years 8 months ago
Coordinating Object Oriented Components Using Data-Flow Networks
We propose a framework for component-based modeling of distributed systems. It provides separation of concerns between computation (in object oriented components), coordination (vi...
Mohammad Mahdi Jaghoori
FMCO
2007
Springer
103views Formal Methods» more  FMCO 2007»
13 years 10 months ago
Safety Guarantees from Explicit Resource Management
We present a language and a program analysis that certifies the safe use of flexible resource management idioms, in particular advance reservation or “block booking” of costl...
David Aspinall, Patrick Maier, Ian Stark
FMCO
2007
Springer
129views Formal Methods» more  FMCO 2007»
13 years 10 months ago
Self Management for Large-Scale Distributed Systems: An Overview of the SELFMAN Project
As Internet applications become larger and more complex, the task of managing them becomes overwhelming. “Abnormal” events such as software updates, failures, attacks, and hots...
Peter Van Roy, Seif Haridi, Alexander Reinefeld, J...
FMCO
2007
Springer
169views Formal Methods» more  FMCO 2007»
13 years 10 months ago
An Object-Oriented Component Model for Heterogeneous Nets
Abstract. Many distributed applications can be understood in terms of components interacting in an open environment. This interaction is not always uniform as the network may consi...
Einar Broch Johnsen, Olaf Owe, Joakim Bjørk...
FMCO
2007
Springer
129views Formal Methods» more  FMCO 2007»
13 years 10 months ago
Causal Semantics for the Algebra of Connectors
Simon Bliudze, Joseph Sifakis
FMCO
2007
Springer
118views Formal Methods» more  FMCO 2007»
13 years 10 months ago
Coordination: Reo, Nets, and Logic
This article considers the coordination language Reo, a Petri net variant called zero-safe nets, and intuitionistic temporal linear logic (ITLL). The first part examines the seman...
Dave Clarke
FMCO
2007
Springer
13 years 10 months ago
COSTA: Design and Implementation of a Cost and Termination Analyzer for Java Bytecode
This paper describes the architecture of costa, an abstract interpretation based cost and termination analyzer for Java bytecode. The system receives as input a bytecode program, (...
Elvira Albert, Puri Arenas, Samir Genaim, German P...
FMCO
2007
Springer
13 years 10 months ago
Universe Types for Topology and Encapsulation
The Universe Type System is an ownership type system for object-oriented programming languages that hierarchically structures the object store; it is used to reason modularly about...
Dave Cunningham, Werner Dietl, Sophia Drossopoulou...