EdShare
Home
Browse
By Year
By Author
Tags
Course code
University structure
Share
About
Help
Login
Login
Browse by Tags: formal methods
Up a level
Export as
ASCII Citation
BibTeX
Dublin Core
EP3 XML
EndNote
Export::Xapian plugin is missing the name parameter
HTML Citation
JSON
METS
Multiline CSV
Object IDs
OpenURL ContextObject
RDF+N-Triples
RDF+N3
RDF+XML
Refer
Reference Manager
Zip
Atom
RSS 1.0
RSS 2.0
Number of items:
59
.
COMP1216 - AY2023-24 - Coursework 2
Event-B Model for a Dentist Appointment System
Shared with the University by
Dr Son Hoang
COMP1216 - An Exercise in Modelling using Relations
Shared with the University by
Dr Son Hoang
COMP1216 - Coursework - An Auction System
Shared with the University by
Dr Son Hoang
COMP1216 - Coursework 2 (2020-21)
Description of Coursework 2 for COMP1216 (2020-21)
Shared with the University by
Dr Son Hoang
COMP1216 - Extending Access Control Model with Tokens and Time
Shared with the University by
Dr Son Hoang
+1 more...
COMP1216 - Extending Event-B Model
Shared with the University by
Dr Son Hoang
+1 more...
COMP1216 - Lab 05 - Modelling with Sets in Event-B
Modelling with Sets in Event-B
Shared with the University by
Dr Son Hoang
+1 more...
COMP1216 - Lab 6 - Modelling with Relations in Event-B
Modelling using Relations in Event-B
Shared with the University by
Dr Son Hoang
+1 more...
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
+1 more...
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
+2 more...
COMP1216 - Lab 9 - Port Management System in Event-B
Port Management system in Event-B
Shared with the University by
Dr Son Hoang
COMP1216 - Lecture 07 - Introducing Event-B
Introducing Event-B (Contexts, machines)
Shared with the University by
Dr Son Hoang
COMP1216 - Modelling Classes and Associations
Shared with the University by
Dr Son Hoang
COMP1216 - Proof-based Verification in Event-B
Shared with the University by
Dr Son Hoang
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
COMP1216 - Revision
Revision
Shared with the University by
Dr Son Hoang
COMP1216 - Solving Puzzles with Invariants
- "Chameleons of three colours" riddle
Shared with the University by
Dr Son Hoang
COMP1216 - What Next? ... How about Program Verification?
Shared with the University by
Dr Son Hoang
COMP1216 Coursework 2 (AY2022-23)
Coursework 2: Event-B modelling of an auction system
Shared with the University by
Dr Son Hoang
COMP1216 Software Modelling and Design (AY2020-21)
Shared with the University by
Dr Son Hoang
COMP2214 - Coursework AY2022-23
Shared with the University by
Dr Son Hoang
COMP2214 - Coursework AY2023-24
MULTI elevator coursework
Shared with the University by
Dr Son Hoang
COMP2214 - Coursework descriptions 2020-21
Shared with the University by
Dr Son Hoang
COMP2214 - Lecture 00 - Introduction
Introduction to Advanced Software Modelling & Design
Shared with the University by
Dr Son Hoang
+1 more...
COMP2214 - Lecture 01 - Proof-based verification in Event-B
Proof-based Verification in Event-B
Shared with the University by
Dr Son Hoang
+1 more...
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
COMP2214 - Lecture 03 - Deductive Proof (First-Order Logic and Set Theory)
Shared with the University by
Dr Son Hoang
+1 more...
COMP2214 - Lecture 04 - Set Theory
A refresher on Set Theory
Shared with the University by
Dr Son Hoang
COMP2214 - Lecture 05 - Tree File
- Tree file system - Transitive Closure
Shared with the University by
Dr Son Hoang
+1 more...
COMP2214 - Lecture 06 - Reachability in Transition System
Shared with the University by
Dr Son Hoang
+1 more...
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
+1 more...
COMP2214 - Lecture 08 - Extension Refinement
- Abstraction & Refinement - Extension Refinement
Shared with the University by
Dr Son Hoang
+1 more...
COMP2214 - Lecture 09 - Extension Refinement with Guard Modification
Shared with the University by
Dr Son Hoang
+1 more...
COMP2214 - Lecture 10 - Data Refinement
Shared with the University by
Dr Son Hoang
+2 more...
COMP2214 - Lecture 11 - An Elevator System
Shared with the University by
Dr Son Hoang
COMP2214 - Lecture 13 - Contracts
Slides from Prof Michael Butler
Shared with the University by
Dr Son Hoang
COMP2214 - Lecture 14 - Loops
Reasoning about looping programs
Shared with the University by
Dr Son Hoang
COMP2214 - Lecture 15 - Introduction to Ada
Introduction to Ada programming language
Shared with the University by
Dr Son Hoang
+6 more...
COMP2214 - Lecture 15 - Verification in Dafny
Verification in Dafny
Shared with the University by
Dr Son Hoang
+2 more...
COMP2214 - Lecture 16 - Event-B to Dafny
Shared with the University by
Dr Son Hoang
COMP2214 - Lecture 16 - Introduction to SPARK
Introductory slides on SPARK
Shared with the University by
Dr Son Hoang
COMP2214 - Lecture 17 - System Theoretic Process Analysis
Shared with the University by
Dr Son Hoang
COMP2214 - Lecture 18 - Requirements Engineering
Shared with the University by
Dr Son Hoang
COMP2214 - Lecture 21 - Revision
Revision lecture
Shared with the University by
Dr Son Hoang
COMP2214 - Problem Class 00 - Introduction to the Rodin Platform
Shared with the University by
Dr Son Hoang
+2 more...
COMP2214 - Problem Class 01 - Deductive Proof (Propositional Logic)
Exercises for Propositional Logic Proof in Rodin Platform
Shared with the University by
Dr Son Hoang
+6 more...
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
+2 more...
COMP2214 - Problem Class 03 - Model a Routing System
Model a Routing System using transitive closure
Shared with the University by
Dr Son Hoang
+2 more...
COMP2214 - Problem Class 04 - Fixing models using failing proofs
Fixing models using failing proofs
Shared with the University by
Dr Son Hoang
+4 more...
COMP2214 - Problem Class 05 - Extension Refinement with Guard Modification
Shared with the University by
Dr Son Hoang
COMP2214 - Problem Class 06 - Hoare Logic
Exercises on Hoare Logic
Shared with the University by
Dr Son Hoang
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
+1 more...
COMP2214 - Problem Class 08 - Elevator System in SPARK
Exercise using the Elevator System in SPARK
Shared with the University by
Dr Son Hoang
COMP2214 - Proof rules
Some useful proof rules
Shared with the University by
Dr Son Hoang
+5 more...
COMP2214 - Tutorial 6 - Verification with Dafny (part 1)
Shared with the University by
Dr Son Hoang
+4 more...
COMP2214 - Tutorial 7 - Verification with Dafny (part 2)
Shared with the University by
Dr Son Hoang
COMP2214 Advanced Software Modelling and Design
Shared with the University by
Dr Son Hoang
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
+2 more...
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
.