Collection items
![[img]](/style/images/fileicons/text.png)
|
COMP2214 - Lecture 00 - Introduction
Introduction to Advanced Software Modelling & Design
Shared with the University by
Dr Son Hoang
|
|
|
COMP2214 - Lecture 01 - Proof-based verification in Event-B
Proof-based Verification in Event-B
Shared with the University by
Dr Son Hoang
|
|
|
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
|
![[img]](/style/images/fileicons/archive.png)
|
COMP2214 - Lecture 05 - Tree File
- Tree file system
- Transitive Closure
Shared with the University by
Dr Son Hoang
|
|
|
COMP2214 - Lecture 04 - Set Theory
A refresher on Set Theory
Shared with the University by
Dr Son Hoang
|
|
|
COMP2214 - Lecture 06 - Reachability in Transition System
Shared with the University by
Dr Son Hoang
|
|
|
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
|
|
|
|
|
|
COMP2214 - Lecture 08 - Extension Refinement
- Abstraction & Refinement
- Extension Refinement
Shared with the University by
Dr Son Hoang
|
|
|
COMP2214 - Problem Class 04 - Fixing models using failing proofs
Fixing models using failing proofs
Shared with the University by
Dr Son Hoang
|
|
|
COMP2214 - Lecture 09 - Extension Refinement with Guard Modification
Shared with the University by
Dr Son Hoang
|
|
|
|
|
|
COMP2214 - Problem Class 05 - Extension Refinement with Guard Modification
Shared with the University by
Dr Son Hoang
|
|
|
|
|
|
COMP2214 - Lecture 12 - Convergence and Deadlock-freeness
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 - Verification in Dafny
Verification in Dafny
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 15 - Introduction to Ada
Introduction to Ada programming language
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 - 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
|
|
|
COMP2214 - Problem Class 00 - Introduction to the Rodin Platform
Shared with the University by
Dr Son Hoang
|
|
|
COMP2214 - Problem Class 01 - Deductive Proof (Propositional Logic)
Exercises for Propositional Logic Proof in Rodin Platform
Shared with the University by
Dr Son Hoang
|
|
|
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
|
|
|
COMP2214 - Problem Class 03 - Model a Routing System
Model a Routing System using transitive closure
Shared with the University by
Dr Son Hoang
|
![[img]](/style/images/fileicons/slideshow.png)
|
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
|
|
|
COMP2214 - Problem Class 08 - Elevator System in SPARK
Exercise using the Elevator System in SPARK
Shared with the University by
Dr Son Hoang
|
|
|
COMP2214 - Coursework descriptions AY2021-22
Coursework descriptions for MULTI elevator system.
Shared with the University by
Dr Son Hoang
|
|
|
|
|
|
COMP2214 - Coursework AY2023-24
MULTI elevator coursework
Shared with the University by
Dr Son Hoang
|
COMP2214 Advanced Software Modelling and Design
| Added By: |
Dr Son Hoang
|
|---|---|
| Date Added: | 29 Jan 2019 15:17 |
| Tags: | software engineering, formal methods |
| Viewing permissions: | University |
| Link: | http://edshare.soton.ac.uk/id/eprint/19730 |
| Downloads & Views |  |
 |