S458/558 FORMAL METHODS FOR PROGRAM
VERIFICATION
SPRING 2015
Lecturer: James F. Lynch
Office: SC 366
email: jlynch@clarkson.edu
Office hours: M
10:00AM-12:00PM, TR 9:30AM-11:00AM
Lecture hours: TR 11:00AM-12:15PM SC334
Text: Logic in Computer Science: Modelling and Reasoning about Systems, 2nd
Edition
by Michael R. A. Huth and Mark D. Ryan.
ISBN: 0-521-54310-X
SYLLABUS
Fundamentals of program specification and
verification (Chapters 1.1–1.5, 2.1–2.4, and 3.1–3.4 in the
text).
Alloy Analyzer (documentation and software from MIT).
NuSMV Symbolic Model Checker (documentation and
software from Trento University)
GRADING
Grading will be based on homework, exams, and a final project. There will not be a final exam.
Homework 5%
3 exams 75%
Project 20%
Exam Dates
Thursday February 5 Solutions
Thursday March 5 Solutions
Thursday April 9 Solutions
You can do the homework assignments with a partner. If you do, both of your names should appear on what you turn in.
The choice of project is up to you (subject to my approval). Some suggestions are below. You can work on it with a partner.
Homework and projects that are done with a partner will be graded using the same standards as work done individually.
Exams, of course, must represent individual effort. Plagiarism of any form will result in a 0 on the exam for the first infraction and an F for the course for any repeated infractions.
Missing an exam without a valid excuse will result in a 0 for the exam. Here are a few examples of invalid excuses:
· My alarm didn’t go off.
· I forgot.
· I broke up with my girl/boyfriend.
· I had a job trip. If you already have a job trip scheduled for the day of an exam, you must let me know during the first two weeks of the semester.
HOMEWORK ASSIGNMENTS
* You can do these informally by saying what the LTL or CTL formula means in English, and then explaining why it is true or false in the model. Or, you can write a NuSMV program with specs that will automatically answer whether the formula is true or false.
PROJECTS
James Anziano & Greg Werbowsky:
Traffic Light System (Alloy and NuSMV)
Nick Bayer &
Kevin Carr: Round Robin (Alloy and NuSMV)
Kristian Brown & Brandon Cornell: Traffic Light
System (Alloy and NuSMV)
Paul Burgwardt & Ryan Parece:
Traffic Light System (Alloy and NuSMV)
Ryan Domina: Round Robin (Alloy), Barbershop (NuSMV)
William Freitag & John Whiddon:
Traffic Light System (Alloy and NuSMV)
Patrick Gulrajani & Emily Kinel:
Dining Philosophers (Alloy and NuSMV)
James Lamphere: Traffic Light System (Alloy and NuSMV)
Alex Macri: Dining Philosophers (Alloy and NuSMV)
Sean McTigue: Cigarette Smokers Problem (Alloy and NuSMV)
Corey Richardson:
Readers and Writers (Alloy and NuSMV)
Scot Tucker: Modeling
Trust Relationships (Alloy), Round Robin (NuSMV)
PROJECT SCHEDULE
March 31: For each project (Alloy and NuSMV), let me know if you are working by yourself or with
a partner. You can work by yourself on both projects,
or with a partner on both, or by yourself on one project and a partner on the
other. You can have different partners on the two projects.
Also, if you’ve decided what
your projects will be about, let me know. If you haven’t, we can discuss
it that week.
SCHEDULE OF MEETINGS
(EACH TEAM SHOULD CHOOSE ONE TIME EACH WEEK, FCFS)
Tuesday, April 14
11:00
11:12
11:24
11:36
11:48
12:00
Thursday, April 16
11:00 Nick Bayer & Kevin Carr
11:12 Kristian
Brown & Brandon Cornell
11:24
11:36
11:48 Patrick Gulrajani
& Emily Kinel
12:00 James Anziano
& Greg Werbowsky
Tuesday, April 21
11:00
11:12 Patrick Gulrajani
& Emily Kinel
11:24
11:36
11:48
12:00 James Anziano
& Greg Werbowsky
Thursday, April 23
11:00
11:12 Kristian
Brown & Brandon Cornell
11:24
11:36
11:48
12:00
Schedule of project demos (during finals week or earlier if you are
ready):
Scheduled on a FCFS basis.
SUGGESTED PROJECTS
LINKS