COMP 525 HOME PAGE
Winter 2012

Instructor: Prakash Panangaden

E-mail: prakash AT cs DOT mcgill DOT ca
Office: McConnell 105 North
Office Phone: (514) 398-7074
Classroom:
Class Times: The class is over.
Office Hours: No more office hours.
TA: Giulia Alberini

Course Introduction and Schedule

A brief docuemnt describing the course and giving the lecture by lecture schedule is available here (pdf format).

Announcements

The prize for the best talk is shared by Joshua Aaron and Etienne Perot. The votes were tied. Congratulations to both. Honourable mentions go to Costin Badescu, Francisco Ferreira-Ruiz and Andrew Cave.
Final grades are ready and have been entered into Minerva. The distribution is: A: 9, A- : 1, B+: 2, B-: 1 and F: 1. I will be out of town from Wednesday to Sunday. You can pick up your evaluations, term paper etc. next week.
Presentation schedule:
- Friday 30th March 9:30-10:30: Andrew Cave: Model checking as proof search and Francisco Ferreira: Using LTL as a type system.
- Wednesday 11th April 9:30-10:30: Amrinder Brar: Other models of omega automata and Ismail Badawi: Alternating automata and verification. Venue: regular classroom.
- Thursday 12th April 10:00-11:30: Gabriel Gaudreault: Expresssive power of modal mu-calculus, Joshua Aaron: Infinite games, and David Thibodeau: The topology of sets recognized by Buchi automata. Venue: Room 320 McConnell.
- Thursday 12th April 3:00-4:30: Costin Badescu: The Jonsson-Tarski Theorem, Antonio Urbano: Model checking large systems and Jonathan Pitre: Model checking in industry. Venue: Room 103 McConnell.
- Friday 13th April 9:30-10:30: Esma Balkir: Complementation using alternation and Ireen Kashem: Tree automata.
- Monday 16th April 9:00-10:30: Elizabeth Hale: The AVISPA tool, Etienne Perot: The Needham-Schroder protocol: model checking and security, Nicolas Pepin-Perrault: Model checking vs theorem proving. Venue: regular classroom. Note the early start.
Check out the web page of the Workshop on The Unusual Effectiveness of Logic in Computer Science for some interesting talks on the importance of logic in computer science.
A proof of the fact that if the finite traces of two finitely branching transition systems are the same then all the traces are the same.
Some notes on strings.
Bisimulation and logical characterization (revised).

Homeworks and Solutions

Assignment 1.
Solutions to Assignment 1.
Assignment 2.
Assignment 3 is due on the 12th of March in class at the start of the class.

Academic Integrity

McGill University values academic integrity. Therefore, all students must understand the meaning and consequences of cheating, plagiarism and other academic offences under the Code of Student Conduct and Disciplinary Procedures: see www.mcgill.ca/integrity for more information.

26th Feb 2012

COMP 525 HOME PAGE Winter 2012