"formal" Methods Forum
Members of the "formal" Methods Forum can now be mailed
via the mailing list:
formal
Overview
The
"formal" Methods Forum has been set up to bridge the gap
between existing research groups in the department. (Here, "formal" is used as
opposed to "informal", i.e. including any mathematical formalization such as
statistical analysis.) It builds on a shared interest in formal methods
especially when applied to safety-critical and real-time systems, and aims to
facilitate and encourage collaboration of group members. Group activities
include the presentation and discussion of ongoing research and latest research
results in the broad area of formal methods.
Research interests of group members include:
- formal verification, automated reasoning, AI
- software reliability and reliability assessment
- software design methods, software testing
- statistical and logical methods
- languages and compilers
- concurrent and communicating systems
- quantitative protocol design
Informal Meetings
To review the current state of our research and to brainstorm new ideas we meet
on Tuesdays at 2:15pm in 3.35 MVB. Meetings started on Tuesday 16 October 2001.
Paper Dissection
Friedger, James E., Greg and Kerstin have formed a "paper dissection" group. We
meet (on demand) on Fridays usually at 3:30pm in 3.19/3.44 with a cup of tea,
coffee, or chocolate and a paper (which was announced at least one week before
the meeting). The paper is then discussed with the aim of understanding it
better. Open questions are sent to the authors for clarification with a
follow-up at the next "dissection" meeting. New members are always
welcome. Please contact one of us for details on the current/next paper.
Current Paper
The next paper will be
``A Calculus Of Broadcasting Systems''
(ps/pdf),
on the 02/11/2001 in MVB-3.19@1500 or
shortly thereafter.
Past Papers
| Date | Title | ps | pdf |
| Tuesday 12/06/2001 | Authentication - Myths and Misconceptions |
email | email |
| Tuesday 05/06/2001 | Defining Liveness |
email | email |
| Tuesday 29/05/2001 | Sooner is Safer than Later |
ps | pdf |
| Tuesday 22/05/2001 | Formalization of Message Sequence Charts | ps | pdf |
| Tuesday 15/05/2001 | How To Make FDR Spin | ps | pdf |
| Tuesday 08/05/2001 | Agents and Roles: Refinement in Alternating-Time Temporal Logic |
email | email
|
| Tuesday 20/03/2001 | Minimal State Graph Generation | ps | pdf |
| Tuesday 13/03/2001 | Efficient Exploration of the SoC Communication Architecture Design Space | ps | pdf |
| Friday 09/02/2001 | Ban Logic - A Logic For Authentication | ps | pdf |
| Friday 02/02/2001 | A Calculus for Cryptographic Protocols - The Spi Calculus | ps | pdf |
| Friday 26/01/2001 | Process Algebra for Performance Evaluation |
ps | pdf |
| Friday 19/01/2001 | Formal Characterisation of Immediate Actions in SPA with Nondeterministic Branching | ps | pdf |
| Friday 12/01/2001 | Symbolic Model Checking for Probabilistic Processes | ps | pdf |
| Friday 15/12/2000 | (Follow up) | | |
| Friday 08/12/2000 | Bisimulation Algorithms for Stochastic Process Algebras and their BDD-based Implementation | ps | pdf |
Seminars
Occasionally we meet for seminars.
The
next seminar will be held on
Tuesday, 4 December
2001, in the VC's Room, Queen's Building at 14:15. The speaker will be
Andy King from the University of Kent at Canterbury. The seminar is entitled
"Fast Boolean Function Manipulation without BDDs".
Guests are always welcome to attend our seminars. Below you can
find the notes of the previous seminars.
Projects
Members
