Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Hoare Logic (CST Part II)
Hoare Logic
Lecturer:Mike Gordon Taken by:Part II Number of lectures: 8 Lecture location: Lecture Theatre 2, WGB Lecture times: 11:00 on Monday, Wednesday and Friday starting on Friday 10 October, 2014
Official web pageSummary: Program specification: partial and total correctness.
Hoare notation. Axioms and rules of Hoare logic. Soundness and
completeness. Mechanised program verification: verification
conditions, weakest preconditions and strongest
postconditions.
Additional topics (only if time):
correct-by-construction methods versus post-hoc verification; proof of
correctness versus property checking; recent developments such as
separation logic.
(Official
syllabus)
Material is examinable if it is presented in lectures!
Examples classes
As there are insufficient supervisors for this course, an examples
class will be conducted by Ramana Kumar between 3pm and 4pm on Monday
November 10 in LT2. For preparation, Ramana suggests you think about:
Updated
handout
(1up). These
will be updated with any changes or corrections made after the start
of lectures.
Slides
The slides presented in the lectures are indicated by a
tick ✓ to the right of the title.
Slides with content that goes beyond what is covered in the 2014/15
course are indicated by a cross ✗.
Remember that the examinable material is what is presented in
lectures.
Microsoft Distinguished Research Lecture by Tony Hoare
entitled Laws of Programming with Concurrency
on 29 January 2015, 4.30-5.30pm at
Microsoft Research Cambridge
(details and registration)