2G1516 2G1521

Formal Methods Formella Metoder

04-05, Dept. of Microelectronics and Information Technology

NEWS - ABOUT THE COURSE - COURSE PM - REQUIREMENTS - SCHEDULE AND SLIDES -STAFF - HELP - SOURCE CODE -TOOLS - LITERATURE AND LINKS - HOWTO - MAILING LIST

Using this page:

This is where to look for all information regarding 2G1516 and 2G1521, autumn term 2004. 

News:

• Returned exams from the August resit are now available at the LECS reception desk, Forum, stair C, level 8.
• August resits. Ordinary resit is on Aug 22, 14-19, look up the exam schedule. A preamble resit is planned for Aug 24, 10-11. It is mandatory to register for the preamble resit with Dilian Gurov (dilian@imit.kth.se) at the latest 2 weeks before the exam date.
• Second resit is on 050110, look up the exam schedule. Last day for registration is Dec. 23. One further, third, preamble resit (last for the 04-05 academic year) is planned for the spring.
• Exam 041918 and reference solutions now available
• Final exam Monday 18 Oct is in rooms 431, 432, 530
• An extra exercise session on CCS is planned for Friday Oct 15, 9-11. Room D
• [ESC/Java Lab]Current schedule for lab reporting can be found here .
• [Spin Lab]Current schedule for lab reporting can be found here .
• [Spin Lab] Some clarifications about the Spin Lab:
  • Regarding property (1-a-iii) in Task 1: "Always, the mobile node eventually talks or moves or timesout" The "timesout" refers to "time runs out", not to the Promela keyword "timeout".
  • If you have difficulty doing simulation with the original model, you can try adding "skip" statements in front of "goto" statements. This solves a bug of the simulator and is NOT needed for verification purposes.
    It is enough to do the following replacements if you are having trouble:
    Replace each "goto Movement;" with "skip; goto Movement;"
    Replace each "goto TimeRunsOut;" with "skip; goto TimeRunsOut;"
    Replace "goto WaitForAdvertisement;" with "skip; goto WaitForAdvertisement;"
• [2G1521 only] An extra preamble exam has been scheduled for 22 Oct, 13.15-14.00, room 437. On 19 Oct, 10-11, room C21, Dilian will give an extra lecture to help preparation for the exam.
• [PVS Lab]Attention!: The lab schedule has been updated.
• [PVS Lab]Current schedule for lab reporting can be found here . The empty time slots will be filled as new groups register.
• Lab panic: If you don't get the lab finished in time for friday it's not the end of the world. There will be a second chance to report the lab after the course has finished. Even if you have not finished do still register for lab reporting tomorrow Friday, to get feedback if nothing else.
• [PVS Lab]Don't forget to do your lab registration by sending a mail to Mika with the names of your group members before Thursday. Each group will get a reply with the demo slot allocated for them on Thursday.
• For 2G1521 Students: SEDS students have access to the so-called "SOC" Lab. On these dual boot machines, RedHat is available where you can install PVS on your own account. You can reach the SOC lab by taking the B elevator to the 8th floor.
• Don't forget to register! This is obligatory for ALL students.
• The mailing list is now activated. All that has sent a request has been approved. If you haven't received an e-mail from majordomo that you have been added to the list, please resend your subscription request as is described below.

About the course:

See also handbook of studies for 2G1516 and 2G1521 respectively.

Formal methods are about rigorous verification of systems. That is, techniques that can help bring about better confidence in the systems we develop and use, beyond what pure testing can achieve. This confidence is brought about, essentially, by analysis in terms of mathematics and logics. In the course we study some important tools and techniques that have been developed for this purpose, their foundations (i.e. how and why they work), and their applications to some concrete case studies (protocols and programs). Part of the message we want to get across is that this stuff can be actually really useful. During the course students will get exposed to four main and complementary schools in the formal methods area, namely, theorem proving, model checking, Hoare logic and weakest precondition calculus, and process algebra.>

The course consists of lectures, exercise sessions, labs, and a final exam. Lectures and exercise sessions are held on the main campus. We have scheduled 12 double lectures and 12 double exercise sessions. Labs are to be done on whatever computer facilities you have available whether personal, at Campus, or at Forum. The only scheduled slots are to get your labs accepted. Make sure you start the labs as early as possible - in most cases not much prior knowledge is required to get started, and you?ll want installation troubles and so forth out of the way well before the lab is due. Also the schedule is tight, and you will find it hard going to catch up once you?re behind.

The course comes in two versions: 2G1516 (5 credits) is the version for the D and IT lines. 2G1521 (6 credits) is the version for the Software Engineering and Distributed Systems international masters program. The difference between the courses is this: 2G1521 starts a week early with an initial refresher module mainly on set notation and first-order logic. After the refresher module the two courses are identical and share lectures, exercises, labs, exams, etc.

Course PM:

Requirements:

Lab reports/presentations and the take-home exam are pass/fail, i.e. they must be produced at the scheduled time, with acceptable quality.

Schedule and Slides:

Labs

You are free to do the labs where it suits you, on own laptops, or in some of the machine halls at Campus or at Forum. For D students, most tools are preinstalled in Stacken. Generally the tools presuppose general c.s.  literacy, including unix/linux and emacs.

Staff:

   Mads Dam, email: mfd at imit.kth.se, phone: 790 4123, mobile: 0708 76 44 40

Course assistants:

    Irem Aktug, email: irem@imit.kth.se, phone: 790 4265, office: 8th floor, Forum building,elevator C. 

    Mika Cohen, email mikac@imit.kth.se, phone: 790 4265, office: 8th floor, Forum building,elevator C. 

Help: