This course requires basic under-graduate background on programming languages as a pre-requisite.
Lectures are 6:30 - 8:30 PM every Friday at COM1 #02-12. The first lecture is on January 18, 2008.
All course materials are being made available to the students via IVLE.
The immense growth in the complexity of software has increased the scope of errors, which are often critical. The nature of these
errors is diverse, resulting from the diversity of the various classes of software: sequential, multithreaded, reactive and real-time.
In this course, we will study techniques for verification, run-time monitoring and debugging of software which help us to give certain
guarantees against such errors. The focus will be on automated validation techniques.
Week 1 : Introduction
Week 2 : Sequential Software Debugging, systematically
Week 3 : Modeling concurrent and distributed software/protocols
Week 4: Property Specification Languages
Week 5: Automated Property Checking of Software
Week 6: The SPIN checker for software validation
Week 7: Midterm (Open Book)
Week 8: Software Abstractions - I
Week 9: Software Abstractions - II
Week 10: Deductive verification
Week 11: PVS theorem prover
Week 12: Software testing
Week 13: Final wrap-up and project presentations
Readings : There are no ideal textbooks for this course.
Readings for every week have been posted under the IVLE Lesson Plan.
Lectures : Lecture notes are being posted every week in the IVLE workbin (see the Lecture Notes folder).
Tools : JSlice debugging tool, SPIN model checker, PVS theorem prover
Students will be required to do a term project.
The project can be individual or in groups of two.
The
project can be a survey or a case study in validation.
Details on sample projects have been posted in IVLE.
Please send email to Abhik if you have any comments/concerns.
Midterm
(open book) : 25 %
Final
(open book) : 50 %
Project
: 25 % Pre-requisites
: Basic undergraduate background in programming languages.
Consultation : Drop by my office anytime or
send me e-mail.
Other Course Information
Instructor:
Abhik Roychoudhury
Office : COM1 #03-20.
Lectures:
Friday 6:30 - 8:30 PM at COM1 #02-12