Andy successfully defends his M.Phil thesis in his Viva. As he is a member of staff he has no internal examiners, but instead two external examiners, David Aspinall and Gerald Luettgen. The session was chaired by Ulrich Berger. Below are some pictures from the Viva and the party afterwards.
The party afterwards was to celebrate Andy's Viva and also to celebrate our technician Sitsofe Wheeler's last day at work. Sitsofe moved on to continue his studies at the University of York.
Temesghen did an internship at Rolls-Royce in Derby. He was part of the System Verification team for the BR725-Control Systems project. His project was to specify in CSP the starting system of the BR725 engine and design test cases to be executed in the rig.
Excursion to the Gower.
Group Meeting: Discussion about specification of the jet engine's control system (part 1 of 2). We set out to specify some of the control systems of a jet engine in CSP-CASL. We were moderately successful in doing this for several aspects of the specification.
Group Meeting: Discussion about specification of the jet engine's control system (part 2 of 2). Below are some photos from the meeting:
Temesghen attends CIE 2008 in Athens where he presents the talk "Implementing Spi Calculus using Nominal techniques".
Markus and Temesghen attend WADT 2008 in Pisa where they present the talks "Refinement notions for CSP-CASL" and "An institution for processes and data". Below are some pictures from the trip.
Gift successfully defends his M.Phil thesis in his Viva. Some pictures of the event and the celebrations afterwards are below:
Christoph Lüth visits Swansea for Gift's viva. Below are some photos from his visit.
Liam submits his final version of the completed M.Phil thesis.
Markus and Temesghen in Berlin. Below are some pictures of the trip.
Glynn Winskel gives talk "Symmetry and Concurrency" at our Colloquia. Below are some pictures from the meal afterwards.
Liam successfully defends his M.Phil thesis in his Viva. His internal examiner was Ulrich Berger and his external was Holger Schlingloff. The session was chaired by Arnold Beckmann. Below are some pictures of the Viva and the celebration afterwards.
Liam and Temesghen attend BCTCS 2008 at Durham University. Temesghen gave the talk "Theory and Application of Testing from CSP-CASL" followed by Liam with the talk "Algorithmic Proof Generation for CSP-CASL-Prover". Below are some pictures from the conference.
Markus and Temesghen visited the company Rolls Royce in Derby. Markus gave a background presentation of CSP-CASL while Temesghen gave a presentation of how to perform formal testing from CSP-CASL.
Group Meeting: An open discussion with Derrick Kourie and Stefan Gruner of the University of Pretoria. Discussed were the research areas of the participants, CSP, CASL and CSP-CASL.
Social gathering in Markus' Office with guests and cake!
Liam and Markus attend a GC6 meeting at the BCS offices in London. Below are some pictures from the trip. The evening before the GC6 meeting we had lunch with Stefan Gruner of the University of Pretoria.
Group Meeting: Temesghen gives the presentation "Linear time - branching time spectrum" part 5 (final).
Group Meeting: Temesghen gives the presentation "Linear time - branching time spectrum" part 4.
Temesghen was invited to give a talk in the PhD seminar at Leicester University.
Group Meeting: Temesghen gives the presentation "Linear time - branching time spectrum" part 3.
Markus holds a large party for Magne Haveraaen with many guests.
Group Meeting: Temesghen gives the presentation "Linear time - branching time spectrum" part 2.
The group attends the department's Theory Away Day at Sketty Hall. Below are some photos from the meeting.
Group Meeting: Markus gives the presentation "Complete Trace Semantics and Failure Semantics".
A happy day for Liam where we all went to the local pub (Pub on the Pond) to celebrate.
Group Meeting: Temesghen gives the presentation "Linear time - branching time spectrum" part 1.
Abstract: We survey various semantics in the linear time - branching time spectrum in a uniform, model - independent way.
Group Meeting: Markus gives a presentation on "Orthodoxies".
Markus attends a meeting of the IFIP WG 1.3 on System Specification as an observer and gives a presentation "Towards Testing from CSP-CASL Specifications".
Markus attends the GC6 meeting in London.
Group Meeting: Markus completes his talk on Full Abstraction in CSP.
Group Meeting: Markus presents the last part of his Gregynog lecture on proving completeness for propositional logic.
The group celebrates Christmas at the traditional "Christmas Concert" at Swansea Museum where Markus plays the Oboe and Piano.
Group Meeting: Holger speaks about "Testing embedded Systems".
Holger Schlingloff visits Swansea for a course on Testing. Below are some photos taken throughout his visit.
Our group organises the 2nd International Workshop on Process and Data at Gregynog. Below are some photos of the event where the following presentations were made :-
Speaker: Andy Gimblett
Title: "The static semantics of CSP-CASL"
Abstract: We present the static semantics of CSP-CASL using Natural Semantics, following the style of the CASL Reference Manual.
Speaker: Gift Samuel
Title: "Semantics of Stable Revivals Models in CSP Prover"
Abstract: In talk, I explain the semantics function of the stable revivals model. Then I will explain how I implemented it in CSP Prover. Finally I discuss about the type correctness(well definedness) and how it is used.
Speaker: Liam O'Reilly
Title: "Three Different Implementation Possibilities for a CSP-CASL-Prover"
Abstract: During this talk I will outline what are deep, semi-deep and shallow encodings in the setting of CSP-CASL-Prover and how these lead to three different possibilities for implementing a CSP-CASL-Prover. Also discussed is the implications of the encoding which HETS produces and what a deep encoding might look like.
Speaker: Markus Roggenbach
Title: "A bit of propositional logic - Part I "
Abstract: We define the language of propositional logic, give its semantics, and define a calculus for it. This gives rise to the question if the calculus captures the defined semantics.
Speaker: Markus Roggenbach
Title: "A bit of propositional logic - Part II"
Abstract: We study how the calculus relates to the semantics defined. It turns out, that the calculus is sound and complete. Full proofs will be given.
Speaker: Temesghen Kahsai
Title: "A year full of Refinement"
Abstract: In this talk I will illustrate some notions of refinement in Algebraic Specification by giving concrete examples. Moreover I will show the decomposition of CSP-CASL refinement, and what kind of examples are we trying to capture using "refinement + hiding " in CSP-CASL.
Group Meeting: Liam and Temesghen present further chapters of the book "How to prove it".
The Theory Away Day, where (almost) the entire Theory Group of the Computer Science Department at Swansea University travels to Hay-on-Wye to hold the annual Theory Away Day. Roughly an army of 20 theoretical computer scientists invade the town and peacefully wonder around the book shops in search of interesting literature. Below are some pictures of our expedition.
Group Meeting: Gift presents another chapter of the book "How to prove it".
Group Meeting: Andy gives a talk on detecting local top elements, Liam and Temesghen report on their visit to York.
Liam and Temesghen attend the BSC conference: Formal-Lite RE in York, UK.
Temesghen gives the presentation "Representing Binders: The Nominal Approach" at the MRes seminar.
Markus visits Magne Haveraaen in Bergen where Markus gives the talk "CSP - new insights into an old paradigm" in the departmental seminar of Computer Science at the University of Bergen.
Markus gives the presentation "Specifying in CASL -- Proving with HETS" in the SAGA / Sophus meeting on 18.10.2007.
Here are some of the Pictures taken from this trip.
Markus presents the paper "Reasoning on Responsiveness -- Extending CSP-Prover by the Model R" (Authors: D. Gift Samuel, Yoshinao Isobe and Markus Roggenbach) at NWPT 2007 in Olso, Norway.
Below are some of the photos taken during this trip where Erwin (the Frog !) was quite active and can be seen in several photos.
Markus and Temesghen attend the 5th IEEE International conference on Software Engineering and Formal Methods (SEFM 07) held in London, UK. Where Temesghen presents the paper "Specification-based Testing for Refinement" (Authors: Temesghen Kahsai, Markus Roggenbach and Bernd-Holger Schlingloff).
Group Meeting: Temesghen gives a test talk for SEFM.
Group Meeting: How to prove it, part I - Presentations by Gift, Liam, Temesghen based on the book Daniel J. Velleman: How to Prove It, Amherst College, Massachusetts, 2006.
Markus was guest of Hans-joerg Kreowski at the Research Centre for Log Dynamics and presented the paper "Proof Principles of CSP -- CSP-Prover in Practice" (Authors: Yoshinao Isobe and Markus Roggenbach) at LDIC 2007 in Bremen.
Group Meeting: Liam presents a test talk for CALCO, Gift presents a talk on the encoding of the model R in CSP-Prover.
Temesghen visits the Theorem Proving Group of Tobias Nipkow at Technical University of Munich to explain his work on how to formalise the spi calculus in Isabelle\HOL using the nominal package which is work done under the supervision of Marino Miculan.
The Group's First Birthday
