Differences

This shows you the differences between two versions of the page.

--- start [2010/12/31 16:44] – jonathan
+++ start [2012/01/03 22:53] (current) – jonathan
@@ Line 1: / Line 1: @@
 ~~NOTOC~~
-====== W11-CSE3341M -Introduction to Program Verification  ======
+====== W12-CSE3341M - Introduction to Program Verification  ======
 ===== Lecture Times =====
-  * Tuesdays/Thursday 11.30am-1pm BC-215
+  * Tuesdays/Thursday 11.30am-1pm, CCB115. **Note**: All classes from now on will be in the Software Engineering Laboratory, CSEB2056.
-  * We will be using the [[http://www.event-b.org/platform.html|Rodin]] toolset.
+  * We will be using the [[http://www.event-b.org/platform.html|Rodin]] toolset (also available with Atelier provers/AnimB on the SVN for Windows). For textbook and course slides see [[:textbook|here]].
-  * For textbook and course slides see [[:textbook|here]].
-  * **Important**: See [[https://forum.cse.yorku.ca/viewforum.php?f=134|3341 Forum]] for the latest announcements. Please subscribe. Please read the course outline regularly.
+  * **Important**: Subscribe to: [[https://forum.cse.yorku.ca/viewforum.php?f=168|3341 Forum]] for the latest announcements. Please ask all questions relating to the course material on the forum (not via email). For all other questions, see me during office hours. Read the course outline regularly. See bottom** ↓** of this page for login with your Prism password. Additional maerial is available from the SVN repository (see link in the sidebar, once you have logged on).
-  * Office hours: Tue/Thu 12.45-1.30pm in the SEL (CSE2056)
+  * Office hours:
 ===== Course Description =====
@@ Line 17: / Line 17: @@
-CSE 3341 3.0- Introduction to Program Verification: Every program implicitly asserts a theorem to the effect that if certain input conditions are met then the program will do what its specifications or documentation says it will. Making that theorem true is not merely a matter of luck or patient debugging; making a correct program can be greatly aided by a logical analysis of what it is supposed to do, and for small pieces of code a proof that the code works can be produced hand-in-hand with the construction of the code itself. Good programming style works in part because it makes the verification process easier and this in turn makes it easier to develop more complex algorithms from simple ones. The course will provide an introduction to the basic concepts of formal verification methods. It will also include the use of tools to aid in verification. We will be using the [[http://www.event-b.org/|Event-B]] method and tool.
+CSE 3341 3.0- Introduction to Program Verification: Every program implicitly asserts a theorem to the effect that if certain input conditions are met then the program will do what its specifications or documentation says it will. Making that theorem true is not merely a matter of luck or patient debugging; making a correct program can be greatly aided by a logical analysis of what it is supposed to do, and for small pieces of code a proof that the code works can be produced hand-in-hand with the construction of the code itself. Good programming style works in part because it makes the verification process easier and this in turn makes it easier to develop more complex algorithms from simple ones. The course will provide an introduction to the basic concepts of formal verification methods. It will also include the use of tools to aid in verification.
+We will be using the [[http://www.event-b.org/|Event-B]] method and tool.