Computer Science

P515 Specification and Verification

Credits: 3


Tools and techniques for rigorous reasoning about software and digital hardware. Safety, reliability, security, and other design-critical applications. Decision algorithms. Projects involving the use of automated reasoning, such as model checkers, theorem provers, and program transformation. Credit not given for both CSCI-P 515 and P 415.

  • Course History

      Spring 2014

      Instructor: Daniel Leivant
      Time: Multiple Times
      Location: Multiple Locations
      Course URL (syllabus link or course homepage)
      Course File (syllabus or course advertisement)
      Supplementary Description: P515 combines introductions to three areas: formal logic, specification and verification of imperative programs, and specification of system behaviour. Students registered to the course under the P415 listing would be dispensed of some of the more challenging projects and exam questions, but otherwise the course will be run at the graduate level.

      Spring 2012

      Instructor: Steve Johnson
      Time: 1:00PM-2:15PM Tue, Thu
      Location: Ballantine Hall, Room 005
      Course URL (syllabus link or course homepage)

      Spring 2011

      Instructor: Steve Johnson
      Time: 9:30AM-10:45AM Tue, Thu
      Location: Lindley Hall, Room 102
      Course URL (syllabus link or course homepage)

      Notice: Undefined variable: s_replace in /ip/soic2/wwws/_php/Course.php on line 258