Com S 512: Formal Methods
Instructor
- Samik Basu (sbasu@cs.iastate.edu, 210 Atanasoff)
Meeting Time & Venue
- Class: MWF 12:10-1:00 PM, Sweeney 1160
Text Material & Resources
- Logic in Computer Science: Huth & Ryan
- Model Checking: Clarke, Grumberg & Peled
- Spin Model Checker: Holzmann
- Software Reliability Methods: Peled
- Automated Theorem Proving: Newborn
Syllabus
Propositional & Predicate logic, Logical inference, Temporal logic
(CTL, LTL, CTL*), Kripke structure, Model checking, Labeled transition
system, Process algebra CCS, Modal mu-calculus, Program verification,
Counter-example analysis, Theorem prover basics.
As per the pre-requisites Com S 330 (Discrete Computational Structures),
311 (Algorithms), registered students are assumed to have reasonable
background in logic, set theory, graph/search algorithms.
Course work (subject to discussion)
- Homeworks: 5-6 homeworks will be assigned. Each homework
will have 1 week turn-around deadline. Submission can be delayed by 1
week from the actual submission deadline with 50% penalty for that
homework. Homework submission with any further delay will not be
accepted. Solutions to homeworks will be posted/discussed 10 days
after the actual submission deadline.
- Midterms & Final: 2 Midterms will be held in February and
March. Midterm and Final exams' exact date/time will be announced in
class.
- Projects: See sample
project. Project work will be done in groups. Each group will
write a report (5-8 pages) and present their work in class at the end
of the semester. Groups may be interviewed by the instructor to assess
grades of group-members.
- Grading Policy:
Overall score in the course will be weighted average of the individual
scores.
Academic Dishonesty
Group study and discussion are welcome. However, collaborations of any
form during the exams will not be tolerated. Homeworks must be
individual's original work. Working in groups is only allowed in
projects. Dishonesty will result in F grade.
Disabilities
If you have a documented disability and anticipate needing
accommodations in this course, please meet with your instructor during
the first week of class. Request that the Disabilities Resources staff
send a SAAR form verifying your disability and specifying the
accommodations you will need.
Lecture Materials, Homeworks, Messages on WebCT: Enrolled students
can access WebCT
using their ISU net-ID and same passwd as their iastate.edu
email account.