Differences

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

--- start [2010/01/06 17:19] – jonathan
+++ start [2010/12/31 19:15] (current) – old revision restored jonathan
@@ Line 4: / Line 4: @@
 ===== Lecture Times =====
-Tuesdays/Wednesdays 11.30am-1pm BC-215
+  * Tuesdays/Thursday 11.30am-1pm BC-215
-From the second week of class and onwards, lectures/labs will take place in the Software Engineering Laboratory (SEL) in CSEB2056. There are are 6 workstations in the lab, but you may want to bring your notebook with the [[http://www.event-b.org/platform.html|Rodin]] Eclipse based Event-B system development application installed.
+  * Starting with the class on **Tuesday Jan 12** at 11.30am, **lectures/labs will take place in the Software Engineering Laboratory (SEL) in CSEB2056**. There are are 6 workstations in the lab, but you may want to bring your notebook with the [[http://www.event-b.org/platform.html|Rodin]] toolset installed. During the lectures we will at times be working with the Rodin toolset. Lectures will take place in CSEB2056 until further notice.
- DescriptionCSE 3341 3.0- Introduction to Program Verification =====
+  * For textbook and course slides see [[:textbook|here]].
-**Course description:** 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.
+  * See [[https://forum.cse.yorku.ca/viewforum.php?f=99|3341 Forum]] for the latest announcements. Please subscribe. Please read the course ouline regularly.
-The course will provide an introduction to the basic concepts of formal verification methods. It will also include the use of simple tools to aid in verification.
+  * Office hours: Tue/Thu 12.45-1.30pm in the SEL (CSE2056)
+===== Course Description =====
+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.