Browse by Tags: formal methods

Up a level
Export as [feed] Atom [feed] RSS 1.0 [feed] RSS 2.0
Number of items: 55.
  1. [img] [img]
    COMP1216 - An Exercise in Modelling using Relations
    Shared with the University by
    Dr Son Hoang
  2. [img] [img]
    COMP1216 - Coursework - An Auction System
    Shared with the University by
    Dr Son Hoang
  3. [img]
    COMP1216 - Coursework 2 (2020-21)
    Description of Coursework 2 for COMP1216 (2020-21)

    Shared with the University by
    Dr Son Hoang
  4. [img] [img]
    COMP1216 - Extending Access Control Model with Tokens and Time
    Shared with the University by
    Dr Son Hoang
  5. [img] [img]
    COMP1216 - Extending Event-B Model
    Shared with the University by
    Dr Son Hoang
  6. [img]
    COMP1216 - Lecture 07 - Introducing Event-B
    Introducing Event-B (Contexts, machines)

    Shared with the University by
    Dr Son Hoang
  7. [img] [img]
    COMP1216 - Modelling Classes and Associations
    Shared with the University by
    Dr Son Hoang
  8. [img] [img]
    COMP1216 - Problem Class 5
    Modelling with Sets

    Shared with the University by
    Dr Son Hoang
  9. [img] [img]
    COMP1216 - Problem Class 9
    Shared with the University by
    Dr Son Hoang
  10. [img] [img]
    COMP1216 - Problem class 6
    Modelling using Relations

    Shared with the University by
    Dr Son Hoang
  11. [img] [img]
    COMP1216 - Problem class 7
    Model a hotel reception system in Event-B

    Shared with the University by
    Dr Son Hoang
  12. [img] [img]
    COMP1216 - Problem class 8
    Managing room allocation in multiple hotels

    Shared with the University by
    Dr Son Hoang
  13. [img]
    COMP1216 - Proof-based Verification in Event-B
    Shared with the University by
    Dr Son Hoang
  14. [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
  15. [img] [img]
    COMP1216 - Revision
    Revision

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

    Shared with the University by
    Dr Son Hoang
  17. [img] [img]
    COMP1216 - What Next? ... How about Program Verification?
    Shared with the University by
    Dr Son Hoang
  18. collection
    COMP1216 Software Modelling and Design
    Shared with the University by
    Dr Son Hoang
  19. [img] [img]
    COMP2214 - Coursework descriptions 2020-21
    Shared with the University by
    Dr Son Hoang
  20. [img] [img]
    COMP2214 - Lecture 00 - Introduction
    Introduction to Advanced Software Modelling & Design

    Shared with the University by
    Dr Son Hoang
  21. [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
  22. [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
  23. [img] [img]
  24. [img] [img]
    COMP2214 - Lecture 04 - Set Theory
    A refresher on Set Theory

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

    Shared with the University by
    Dr Son Hoang
  26. [img] [img]
    COMP2214 - Lecture 06 - Reachability in Transition System
    Shared with the University by
    Dr Son Hoang
  27. [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
  28. [img] [img]
    COMP2214 - Lecture 08 - Extension Refinement
    - Abstraction & Refinement - Extension Refinement

    Shared with the University by
    Dr Son Hoang
  29. [img] [img]
  30. [img] [img]
    COMP2214 - Lecture 10 - Data Refinement
    Shared with the University by
    Dr Son Hoang
  31. [img] [img]
    COMP2214 - Lecture 11 - An Elevator System
    Shared with the University by
    Dr Son Hoang
  32. [img]
    COMP2214 - Lecture 13 - Contracts
    Slides from Prof Michael Butler

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

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

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

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

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

    Shared with the University by
    Dr Son Hoang
  41. [img] [img]
    COMP2214 - Problem Class 6 - Hoare Logic
    Exercises on Hoare Logic

    Shared with the University by
    Dr Son Hoang
  42. [img] [img]
    COMP2214 - Problem Class 7 - 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
  43. [img] [img]
    COMP2214 - Problem Class 8 - Elevator System in SPARK
    Exercise using the Elevator System in SPARK

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

    Shared with the University by
    Dr Son Hoang
  45. [img]
    COMP2214 - Tutorial 00 - Introduction to the Rodin Platform
    Shared with the University by
    Dr Son Hoang
  46. [img] [img]
    COMP2214 - Tutorial 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 - Tutorial 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 - Tutorial 03 - Model a Routing System
    Model a Routing System using transitive closure

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

    Shared with the University by
    Dr Son Hoang
  50. [img] [img]
  51. [img] [img]
    COMP2214 - Tutorial 6 - Verification with Dafny (part 1)
    Shared with the University by
    Dr Son Hoang
  52. [img] [img]
    COMP2214 - Tutorial 7 - Verification with Dafny (part 2)
    Shared with the University by
    Dr Son Hoang
  53. collection
    COMP2214 Advanced Software Modelling and Design
    Shared with the University by
    Dr Son Hoang
  54. [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
  55. [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 Sep 26 13:13:57 2021 UTC.