Skip to main navigationSkip to main content
The University of Southampton
6th International ABZ Conference ASM, Alloy, B, TLA, VDM, Z, 2018


Springer LNCS Volume 10817 is available online: LNCS volume for ABZ

Tuesday 5 June

Parallel Workshops: Rodin 2018 and SETS 2018

8:30-9:00 Registration

9:00-9:30 Opening and Welcome

9:30-10:30 Invited Talk

10:30-11:00 Break

Rodin  2018 Workshop Programme  SETS 2018 Workshop Programme

 11:00-12:20 Modelling Tools and Extensions

  • Dana Dghaym, Thai Son Hoang, Colin Snook and Michael Butler. The eXtended Event-B Plug-in XEvent-B
  • Paulius Stankaitis, Alexei Iliasov, Tsutomu Kobayashi, Alexander Romanovsky and Fuyuki Ishikawa. A Framework for Developing Distributed Protocols with Event-B
  • James Snook. A New Language to Construct Algebraic Hierarchies for Event-B
  • G. Dupont, Y. Aït-Ameur, M. Pantel, and N. K. Singh. On the use of the Theory Plug-In to define theories for differential equations

12:20-13:30 Lunch

13:30 -15:20 User Reports and Methods

  • John Colley and Michael Butler. Using Formal Methods to demonstrate Compliance with System Requirements for DO-178C_DO-333
  • Giles Howard, Michael Butler, John Colley and Vladimiro Sasson. Supporting a systems-theoretic co-analysis of safety & security using Event-B & Rodin
  • Ilya Shchepetkov. Using Refinement in Formal Development of OS Security Policy Model
  • Martin Kubisch and Colin Snook. Security Analysis of the 'Touch And Go Assistant' for Aircraft Turn-around
  • Keming Wang and Zheng Wang.  Modeling and Verification of Railway Level Crossing Management System Using Event-B

15:20-16:00 Break

16:00-17:40 Code Generation and Testing

  • Alexei Iliasov. Safecap generic verification framework
  • Mohammadsadegh Dalvandi, Asieh Salehi Fathabadi and Michael Butler. A Report on PRiME Code Generation Activities 
  • Ahmed Al-Brashdi, Michael Butler and Abdolbaghi Rezazadeh. UB2DB Rodin Plug-in for Automated Database Code Generation
  • Tomas Fischer. Formal Model Validation through Acceptance Tests
  • Rupert Schlick and Thorsten Tarrach. Mutation-based test-case generation for Event-B

More details can be found here

11:00-12:20 Session 1 

  • Domenico Cantone and Alberto Policriti. Encoding Sets as Real Numbers
  • Maximiliano Cristiá and Gianfranco Rossi Programming in Java with Restricted Intensional Sets
  • Catherine Dubois and Sulyvan Weppe. Towards Coq Formalisation of {log} Set Constraints Resolution

12:20-13:50 Lunch

13:50 -15:30 Session 2

  • Alberto Casagrande, Francesco Di Cosmo and Eugenio G. Omodeo. Proof-checking and graph connectivity with AEtnaNova
  • Domenico Cantone, Marianna Nicolosi-Asmundo and Daniele Francesco Santamaria. A set-based reasoner for the description logic DLD4,×
  • Olivier Hermant. Polarized Rewriting and Tableaux in B Set Theory
  • Vincent Semeria. HilbertProofs


18:00-19:30 Guided walk around the historic city walls and vaults

19:30-22:30 Meet somewhere for dinner (Not included in the registration fee)


Wednesday 6 June

8:30-09:00 Registration

9:00-10:00 Invited Talk:

10:00-10:30 Short Talks:

10:30-11:00 Break

11:00 – 12:30 Translation and Transformation:

12:30-14:00 Lunch

14:00 -15:00 Invited Talk:

15:00 -15:30 Short Talks:

15:30-16:00 Break

16:00 – 17:30: Analysis and Tests:

17:30 ABZ Steering Committee meeting


Thursday 7 June

9:00-10:00 Invited Talk:

10:00-10:30 Short Talks:

10:30-11:00 Break

11:00 – 12:30 Reals and Hybrid Systems:

12:30-14:00 Lunch

14:00-16:00 Refinement:

16:30 – 23:00 Excursion and Dinner


Friday 8 June

9:00-10:00 Invited Talk:

10:00-10:30 Panel Discussion:

10:30-11:00 Break

11:00-12:30 Hybrid ERTMS Case Study Session 1:

12:30-13:50 Lunch

13:50 -15:30 Hybrid ERTMS Case Study Session 2:

15:30-16:00 Break

16:00-17:15  Short Talks:

17:15 Close



We use cookies to ensure that we give you the best experience on our website. If you continue without changing your settings, we will assume that you are happy to receive cookies on the University of Southampton website.