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



Privacy Settings