Today's formal methods are proof and type systems.
As appetite, we give a very broad outline of interactive theorem proving and a perspective on software correctness of distributed systems.
As starter, we consider freely generated algebraic structures, such as (several varieties of) monoids: CM, PCM, ICM.
The main course of …
Deadlock Detection for Actor-based Coroutines
The actor-based language studied in this research features asynchronous method calls and supports coroutines which allow for the cooperative scheduling of the method invocations belonging to an actor. We model the local behavior of an actor as a well-structured transition system by means of predicate abstraction and derive the decidability …
read moreScheduling of Parallel Applications
Most parallel applications leave the scheduling problem of their constituent processes to a general purpose scheduler, such as an operating system scheduler. Generally, constituent processes of a parallel application interact. For example, one process interacts with another by using its produced data. These interactions of processes introduce dependencies amongst them …
read more2APL: Expressiveness in Concurrency: The Case of Session-Typed Processes
The expressiveness of models of concurrency has intrigued researchers for a number of years now. In particular, studies on the expressiveness of process calculi (such as CCS and the pi-calculus) have had considerable impact. The interest is in questions such as, e.g., under what conditions two process languages C …
read moreInvestigating Cooperative Scheduling in Parallel and Distributed Systems
Our ongoing work focuses on an efficient solution to implement cooperative scheduling models through a user-friendly library written using Java 8. This library translates code written in a modelling language named the Abstract Behavioural Specification Language, into executable Java code. We investigate the issues raised by nested parallelism and the …
read moreEquations and coequations for deterministic automata
In this talk we will define the notion of equations and coequations for deterministic automata and, with the aid of some examples, we define what it means for a deterministic automaton to satisfy a set of equations or coequations. We will show a correspondence between sets of equations and coequations …
read moreComposing Constraint Automata, State-by-State
When composing Constraint Automata by means of the product, one can run into cases where the amount of resources necessary grows exponentially in the number of automata. If the Constraint Automaton being calculated requires an exponential number of states by its very nature, this is not surprising. However, there are …
read moreeScience, Theory and Experience
eScience, or enabling science, involves the theory and practice of how to enable scientists from different domains to take advantage of the latest advancements in computer science and technology. This is mainly achieved via science gateways, also known as virtual research environments, which hide the technical details of accessing and …
read moreVirtual Prototyping for Cyber Physical Systems
Virtual Prototyping is the technology that makes it possible to develop a virtual prototype of a system under design and explore the system design space, including hardware and software. The real application software can be run over the virtual prototype platform and outputs the same results as the real system …
read moreA new method for verification of transition systems is presented - part 2
The state space of a transition system is defined as a quotient set (i.e. a set of equivalence classes) of terms of a top most sort State, and the transitions are defined with conditional rewrite rules over the quotient set. A property to be verified is either (1) an …
read more