In this talk I discuss a mechanism for object creation which allows for an optimal use of bounds on the visible heap in model-checking of object-oriented programs.
read moreOther presentations
Tool demonstration
Software Tools Demonstration
A number of our colleague in SEN3 have been developing software tools in the context of their various projects. Many, but not all, of these tools are related to Reo and are integrated into the Eclipse Coordination Tools (ECT). The ECT also incorporates some tools developed by …
read moreAutomated deadlock detection in synchronized multithreaded call-graphs
In this talk I will discuss automata models for the specification and (automated) analysis of the basic mechanism for synchronizing threads in Java.
read moreIn the Name of the Role (sequel)
This presentation introduces a formalism for the specification of generic behavioral interfaces, so called roles. The main characteristic feature of this formalism is the dynamic creation of processes that act in the name of their roles. I will present a compositional trace semantics of roles which is fully abstract with …
read moreIn the Name of the Role
This presentation introduces a formalism for the specification of generic behavioral interfaces, so called roles. The main characteristic feature of this formalism is the dynamic creation of processes that act in the name of their roles. I will present a compositional trace semantics of roles which is fully abstract with …
read moreFully abstract semantics for OO
The presentation is a part of the MobiJ project meeting.
In this talk we will discuss our ongoing work concerning the problem of a fully abstract semantics for object-oriented languages and its relation with components.
read moreO2C: A Semantic Thread From Objects to Components
In this tutorial we present the basic concepts that underlie object oriented and component based software engineering and their semantic justifications. We start with the basic concepts such as abstract data types and inheritance, as used in the object oriented paradigm to enhance reuse, modularity, and maintenance of software. We …
read moreA proof theory for the multi-threaded flow of control in Java
In this talk I'll give on overview of an assertion proof method for reasoning about threads in Java. The proof method integrates in a modelar manner an intereference freedom test for the shared variable concurrency within an object and the cooperation test for reasoning about method calls.
read moreRecent trends in object oriented verification
I'll discuss an assertional proof method for reasoning about the multi-threaded flow of control in Java. This method combines in a modular manner two well-known proof-methods: the Owicki-Gries method for shared-variable concurrency and the Apt-Francez- de Roever method for CSP.
read more
Page 1 / 1