Home
CMSC 433: Programming Language Technologies and Paradigms
Fall 2024
Lectures:
Monday & Wednesday, 3:30 - 4:45pm
HJP 0226
Description: Students will be introduced to a range of modern formal methods and software engineering practices, focusing on Dafny, SAT solvers, Solver aided programming, and computer aided theorem proving. The first part of the course will look at Dafny, a verification-aware programming language that is used heavily at Amazon: students will learn different techniques for writing down precise specifications of desired system behavior and for proving that specifications hold of software artifacts. The second part of the course will focus on SAT solvers, SMT solvers, and apply these techniques to automatic bug finding and program verification. We will implement a miniature version of Dafny. The third part of the course will focus on the interactive theorem proving. We will learn the basics of the theorem prover Coq. Knowledge of functional programming in the form of OCaml (from 330) is assumed, but not prior knowledge of Dafny.
Recommended Textbook: Program Proofs by K. Rustan M. Leino
Staff:
| Name | Hours (AVW4140 unless stated otherwise) | |
|---|---|---|
| Anwar Mamat | anwar@umd.edu | W 11am-12pm (in-person IRB 2248), Tu 2-3pm on Zoom |
| Jeff Giliberti | jeffgili@umd.edu | MWF 9am-11am |
| Ethan Chou | echou1@umd.edu | MThu 12:30pm-1:30pm, F 2pm-3pm |
| Sai Pranav Theerthala | sptheerthala@umd.edu | Tu 2pm-4pm, Thu 2pm-3pm |
| Samuel Badalov | sbadalov@terpmail.umd.edu | Tu 11am-12pm, F 12pm-2pm |
| Vishal Budamala | vbudamal@terpmail.umd.edu | F 9am-12pm |
Disclaimer: All information on this web page is tentative and subject to change. Any substantive change will be accompanied with an announcement to the class via ELMS.