Diary Year 2: 01.08.2007 - 31.07.2008

16.07.2008

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.

01.07.2008 - 11.08.2008

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.

28.06.2008

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.

27.06.2008

Group Meeting: Discussion about specification of the jet engine's control system (part 2 of 2). Below are some photos from the meeting:

13.06.2008 - 16.06.2008

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.

06.06.2008

Gift successfully defends his M.Phil thesis in his Viva. Some pictures of the event and the celebrations afterwards are below:

04.06.2008

Liam submits his final version of the completed M.Phil thesis.

31.03.2008

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.

19.03.2008

Social gathering in Markus' Office with guests and cake!

12.03.2008

Group Meeting: Temesghen gives the presentation "Linear time - branching time spectrum" part 5 (final).

06.03.2008

Group Meeting: Temesghen gives the presentation "Linear time - branching time spectrum" part 4.

28.02.2008

Group Meeting: Temesghen gives the presentation "Linear time - branching time spectrum" part 3.

14.02.2008

Group Meeting: Temesghen gives the presentation "Linear time - branching time spectrum" part 2.

08.02.2008

The group attends the department's Theory Away Day at Sketty Hall. Below are some photos from the meeting.

07.02.2008

Group Meeting: Markus gives the presentation "Complete Trace Semantics and Failure Semantics".

07.02.2008

A happy day for Liam where we all went to the local pub (Pub on the Pond) to celebrate.

31.01.2008

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.

24.01.2008

Group Meeting: Markus gives a presentation on "Orthodoxies".

13.12.2007

Group Meeting: Markus completes his talk on Full Abstraction in CSP.

06.12.2007

Group Meeting: Markus presents the last part of his Gregynog lecture on proving completeness for propositional logic.

05.12.2007

The group celebrates Christmas at the traditional "Christmas Concert" at Swansea Museum where Markus plays the Oboe and Piano.

29.11.2007

Group Meeting: Holger speaks about "Testing embedded Systems".

18.11.2007 - 19.11.2007

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.

08.11.2007

Group Meeting: Liam and Temesghen present further chapters of the book "How to prove it".

02.11.2007

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.

01.11.2007

Group Meeting: Gift presents another chapter of the book "How to prove it".

25.10.2007

Group Meeting: Andy gives a talk on detecting local top elements, Liam and Temesghen report on their visit to York.

16.10.2007

Temesghen gives the presentation "Representing Binders: The Nominal Approach" at the MRes seminar.

10.10.2007 - 12.10.2007

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.

05.09.2007

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.

 

 

20.08.2007 - 24.08.2007

Liam and Markus attend CALCO 07 held in Bergen, Norway. Liam gives the presentation "Integrating Theorem Proving for Processes and Data" in the CALCO-jnr workshop. Below are some pictures from the trip.

15.08.2007

Group Meeting: Liam presents a test talk for CALCO, Gift presents a talk on the encoding of the model R in CSP-Prover.