CS 5160

Last Updated

  • Schedule of Classes - October 31, 2025 7:07PM EDT

CS 5160
Formal Verification

Course information provided by the 2025-2026 Catalog.

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.


Prerequisites CS 3110 or permission of instructor, proficiency with programming (e.g. CS 2110), and proof (e.g. CS 2800 or a mathematics course numbered 3000 or above).

Last 4 Terms Offered 2022SP

View Enrollment Information

Syllabi: none

  •   Regular Academic Session.  Choose one lecture and one discussion. Combined with: CS 4160

  • 4 Credits Stdnt Opt

  • 16324 CS 5160   LEC 001

  •  
    • TR
    • Jan 20 - May 5, 2026

    • Clarkson, M

  • Instruction Mode: In Person

    For Bowers Computer and Information Science (CIS) Course Enrollment Help, please see: https://tdx.cornell.edu/TDClient/193/Portal/Home/

  • 16325 CS 5160   DIS 201

  •  
    • F
    • Jan 20 - May 5, 2026

    • Clarkson, M

  • Instruction Mode: In Person

  • 16326 CS 5160   DIS 202

  •  
    • F
    • Jan 20 - May 5, 2026

    • Clarkson, M

  • Instruction Mode: In Person