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 Dec 22 06:27:31 2024 UTC
.