Browse by Tags: formal methods

Up a level
Export as [feed] Atom [feed] RSS 1.0 [feed] RSS 2.0
Number of items: 59.
  1. [img] [img]
    COMP1216 - AY2023-24 - Coursework 2
    Event-B Model for a Dentist Appointment System

    Shared with the University by
    Dr Son Hoang
  2. [img] [img]
    COMP1216 - An Exercise in Modelling using Relations
    Shared with the University by
    Dr Son Hoang
  3. [img] [img]
    COMP1216 - Coursework - An Auction System
    Shared with the University by
    Dr Son Hoang
  4. [img]
    COMP1216 - Coursework 2 (2020-21)
    Description of Coursework 2 for COMP1216 (2020-21)

    Shared with the University by
    Dr Son Hoang
  5. [img] [img]
    COMP1216 - Extending Access Control Model with Tokens and Time
    Shared with the University by
    Dr Son Hoang
  6. [img] [img]
    COMP1216 - Extending Event-B Model
    Shared with the University by
    Dr Son Hoang
  7. [img] [img]
    COMP1216 - Lab 05 - Modelling with Sets in Event-B
    Modelling with Sets in Event-B

    Shared with the University by
    Dr Son Hoang
  8. [img] [img]
    COMP1216 - Lab 6 - Modelling with Relations in Event-B
    Modelling using Relations in Event-B

    Shared with the University by
    Dr Son Hoang
  9. [img] [img]
    COMP1216 - Lab 7 - A Hotel Reception System in Event-B
    Model a hotel reception system in Event-B

    Shared with the University by
    Dr Son Hoang
  10. [img] [img]
    COMP1216 - Lab 8 - Multiple Hotel System in Event-B
    Managing room allocation in multiple hotels in Event-B

    Shared with the University by
    Dr Son Hoang
  11. [img] [img]
    COMP1216 - Lab 9 - Port Management System in Event-B
    Port Management system in Event-B

    Shared with the University by
    Dr Son Hoang
  12. [img]
    COMP1216 - Lecture 07 - Introducing Event-B
    Introducing Event-B (Contexts, machines)

    Shared with the University by
    Dr Son Hoang
  13. [img] [img]
    COMP1216 - Modelling Classes and Associations
    Shared with the University by
    Dr Son Hoang
  14. [img]
    COMP1216 - Proof-based Verification in Event-B
    Shared with the University by
    Dr Son Hoang
  15. [img]
    COMP1216 - Relations in Event-B
    Modelling using Relations in Event-B - Order Pairs - Cartesian Product - Relations - Domain/Range of relations - Relational Image

    Shared with the University by
    Dr Son Hoang
  16. [img] [img]
    COMP1216 - Revision
    Revision

    Shared with the University by
    Dr Son Hoang
  17. [img] [img]
    COMP1216 - Solving Puzzles with Invariants
    - "Chameleons of three colours" riddle

    Shared with the University by
    Dr Son Hoang
  18. [img] [img]
    COMP1216 - What Next? ... How about Program Verification?
    Shared with the University by
    Dr Son Hoang
  19. [img] [img]
    COMP1216 Coursework 2 (AY2022-23)
    Coursework 2: Event-B modelling of an auction system

    Shared with the University by
    Dr Son Hoang
  20. collection
    COMP1216 Software Modelling and Design (AY2020-21)
    Shared with the University by
    Dr Son Hoang
  21. [img] [img]
    COMP2214 - Coursework AY2022-23
    Shared with the University by
    Dr Son Hoang
  22. [img] [img]
    COMP2214 - Coursework AY2023-24
    MULTI elevator coursework

    Shared with the University by
    Dr Son Hoang
  23. [img] [img]
    COMP2214 - Coursework descriptions 2020-21
    Shared with the University by
    Dr Son Hoang
  24. [img] [img]
    COMP2214 - Lecture 00 - Introduction
    Introduction to Advanced Software Modelling & Design

    Shared with the University by
    Dr Son Hoang
  25. [img] [img]
    COMP2214 - Lecture 01 - Proof-based verification in Event-B
    Proof-based Verification in Event-B

    Shared with the University by
    Dr Son Hoang
  26. [img] [img]
    COMP2214 - Lecture 02 - Deductive Proof (Propositional Logic)
    - Constructing Proof Trees - Inference Rules - Applying inference rules backwardly to construct proof trees

    Shared with the University by
    Dr Son Hoang
  27. [img] [img]
    COMP2214 - Lecture 03 - Deductive Proof (First-Order Logic and Set Theory)
    Shared with the University by
    Dr Son Hoang
  28. [img] [img]
    COMP2214 - Lecture 04 - Set Theory
    A refresher on Set Theory

    Shared with the University by
    Dr Son Hoang
  29. [img] [img]
    COMP2214 - Lecture 05 - Tree File
    - Tree file system - Transitive Closure

    Shared with the University by
    Dr Son Hoang
  30. [img] [img]
    COMP2214 - Lecture 06 - Reachability in Transition System
    Shared with the University by
    Dr Son Hoang
  31. [img] [img]
    COMP2214 - Lecture 07 - Debugging Models with Proof and Judgement
    Debugging Models with Proof and Judgement - Strengthen Guards - Modify Actions - Strengthen Invariants - Weaken Invariants

    Shared with the University by
    Dr Son Hoang
  32. [img] [img]
    COMP2214 - Lecture 08 - Extension Refinement
    - Abstraction & Refinement - Extension Refinement

    Shared with the University by
    Dr Son Hoang
  33. [img] [img]
    COMP2214 - Lecture 09 - Extension Refinement with Guard Modification
    Shared with the University by
    Dr Son Hoang
  34. [img] [img]
    COMP2214 - Lecture 10 - Data Refinement
    Shared with the University by
    Dr Son Hoang
  35. [img] [img]
    COMP2214 - Lecture 11 - An Elevator System
    Shared with the University by
    Dr Son Hoang
  36. [img]
    COMP2214 - Lecture 13 - Contracts
    Slides from Prof Michael Butler

    Shared with the University by
    Dr Son Hoang
  37. [img]
    COMP2214 - Lecture 14 - Loops
    Reasoning about looping programs

    Shared with the University by
    Dr Son Hoang
  38. [img] [img]
    COMP2214 - Lecture 15 - Introduction to Ada
    Introduction to Ada programming language

    Shared with the University by
    Dr Son Hoang
  39. [img] [img]
    COMP2214 - Lecture 15 - Verification in Dafny
    Verification in Dafny

    Shared with the University by
    Dr Son Hoang
  40. [img] [img]
    COMP2214 - Lecture 16 - Event-B to Dafny
    Shared with the University by
    Dr Son Hoang
  41. [img] [img]
    COMP2214 - Lecture 16 - Introduction to SPARK
    Introductory slides on SPARK

    Shared with the University by
    Dr Son Hoang
  42. [img]
    COMP2214 - Lecture 17 - System Theoretic Process Analysis
    Shared with the University by
    Dr Son Hoang
  43. [img]
    COMP2214 - Lecture 18 - Requirements Engineering
    Shared with the University by
    Dr Son Hoang
  44. [img] [img]
    COMP2214 - Lecture 21 - Revision
    Revision lecture

    Shared with the University by
    Dr Son Hoang
  45. [img]
    COMP2214 - Problem Class 00 - Introduction to the Rodin Platform
    Shared with the University by
    Dr Son Hoang
  46. [img] [img]
    COMP2214 - Problem Class 01 - Deductive Proof (Propositional Logic)
    Exercises for Propositional Logic Proof in Rodin Platform

    Shared with the University by
    Dr Son Hoang
  47. [img] [img]
    COMP2214 - Problem Class 02 - Deductive Proof (Predicate Logic and Set Theory)
    Exercises for Predicate Logic and Set Theory Proof in Rodin Platform

    Shared with the University by
    Dr Son Hoang
  48. [img] [img]
    COMP2214 - Problem Class 03 - Model a Routing System
    Model a Routing System using transitive closure

    Shared with the University by
    Dr Son Hoang
  49. [img] [img]
    COMP2214 - Problem Class 04 - Fixing models using failing proofs
    Fixing models using failing proofs

    Shared with the University by
    Dr Son Hoang
  50. [img] [img]
    COMP2214 - Problem Class 05 - Extension Refinement with Guard Modification
    Shared with the University by
    Dr Son Hoang
  51. [img] [img]
    COMP2214 - Problem Class 06 - Hoare Logic
    Exercises on Hoare Logic

    Shared with the University by
    Dr Son Hoang
  52. [img] [img]
    COMP2214 - Problem Class 07 - Hoare Logic in SPARK
    Exercises on Hoare Logic in SPARK - Flow analysis - Pre-/Post-conditions - Loops: Invariants, Variants

    Shared with the University by
    Dr Son Hoang
  53. [img] [img]
    COMP2214 - Problem Class 08 - Elevator System in SPARK
    Exercise using the Elevator System in SPARK

    Shared with the University by
    Dr Son Hoang
  54. [img]
    COMP2214 - Proof rules
    Some useful proof rules

    Shared with the University by
    Dr Son Hoang
  55. [img] [img]
    COMP2214 - Tutorial 6 - Verification with Dafny (part 1)
    Shared with the University by
    Dr Son Hoang
  56. [img] [img]
    COMP2214 - Tutorial 7 - Verification with Dafny (part 2)
    Shared with the University by
    Dr Son Hoang
  57. collection
    COMP2214 Advanced Software Modelling and Design
    Shared with the University by
    Dr Son Hoang
  58. [img] [img]
    COMP2214 Lecture - Event-B to SPARK
    This lecture about data refinement from Event-B models and generating SPARK/Ada from the model

    Shared with the University by
    Dr Son Hoang
  59. [img] [img]
    Modelling Dojo: The SmarTaxi Case Study
    We illustrate the modelling activities using the SmarTaxi Case Study

    Shared with the University by
    Dr Son Hoang
This list was generated on Sun Oct 6 16:39:09 2024 UTC.