CS 4160

CS 4160

Course information provided by the Courses of Study 2021-2022.

An introduction to formal verification, focusing on correctness of functional and imperative programs relative to mathematical specifications. Topics include computer-assisted theorem proving, logic, programming language semantics, and verification of algorithms and data structures. Assignments involve extensive use of a proof assistant to develop and check proofs.

When Offered Spring.

Prerequisites/Corequisites Prerequisite: CS 3110 or permission of instructor. Students are expected to be proficient with programming (e.g. CS 2110), and proof (e.g. CS 2800 or a mathematics course numbered 3000 or above).

Distribution Category (SMR-AS)

View Enrollment Information

Syllabi:
  •   Regular Academic Session.  Choose one lecture. Discussion optional. Combined with: CS 5160

  • 4 Credits Stdnt Opt

  • 18790 CS 4160   LEC 001

  • Instruction Mode: In Person
    Enrollment reserved for CIS students only. All other students must add themselves to the waitlist during add/drop in January.

  • 19231 CS 4160   DIS 201

    • F Phillips Hall 203
    • Jan 24 - May 10, 2022
    • Clarkson, M

  • Instruction Mode: In Person
    This discussion section is not mandatory.

  • 19232 CS 4160   DIS 202

  • Instruction Mode: In Person
    This discussion section is not mandatory.