We begin with a brief introduction to coalgebras for an endofunctor and discuss the duals of Birkhoff's variety theorem and the quasi-variety theorem. These theorems suggest a notion of coequations for categories of coalgebras. Namely, we take coequations to be predicates over the carrier of cofree coalgebras, where coequation satisfaction …
read moreVerification of security protocols using Casper and FDR
Security protocols are relatively small and need to be right. One can interpret these protocols as messages exchanged between agents that might be intercepted or altered by an intruder. Therefore, a security protocol can be represented as a system of parallel CSP processes that correspond to the agents and intruder …
read moreCoalgebraic Modalities and Logics for Process Transformations
Starting originally from my previous work on formalizing "epistemic actions" (joint work with L. Moss and S. Solecki), I have been recently working on logics for process transformations. A process transformation is a partial map from processes to processes, with the property that it's bisimulation-preserving: bisimilar processes are mapped to …
read moreTowards a Formal Specification of Reo
In this talk, we discuss our on-going work on the formal specification of Reo. Reo is a paradigm for composition of software components based on the notion of mobile channels. The main focus of attention in Reo is the channels and operations on them, not the processes that operate on …
read moreAutomatic generation of proof-outline for Java
Marcel Kyas will present his work on the project MobiJ and Omega.
In this talk I will present a tool generating proof-outline as PVS theories from a Java class.
read moreModal Properties as Natural Transformations
Since there will be enough time, I will use the opportunity to start the talk with a general introduction to natural transformations and examples of applications in computer science.
The semantics of a modal formula is an operation assigning to any model (Kripke frame) A, to any valuation of atomic …
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 moreCoinductive counting with weighted automata and continued fractions - part 2
We shall elaborate on Sections 13-17 of the recently appeared CWI report
Elements of stream calculus (an extensive exercise in coinduction) SEN-R0120
by treating a number of additional examples of what could be called `coinductive counting'. The main idea is to enumerate the structures to be counted (such as binary …
read moreOn Coequations
Joint work with Jiri Rosicky, Brno.
Lawvere introduced the idea to consider as equations expressions t=t' where t,t' are natural transformations U^n-->U, U being the forgetful functor U:Alg-->Set. This idea is dualised to coalgebras, and differences and analogies to the algebraic case are dicussed …
read moreHorn coequations
We give a brief summary of the Horn variety, quasivariety and Birkhoff variety theorems (using the H, S, P and P+ closure operators) for categories of algebras for an endofunctor and dualize these results to yield formally dual theorems for categories of coalgebras. While the notions of coequations and conditional …
read more