Princeton University
Computer Science Department

COS 598A: Advanced Topics in Computer Science
Advances in Verification

Aarti Gupta

Spring 2018

Course Description

This seminar explores selected topics in recent applications of automatic verification techniques to reasoning about ML (machine learning) components and systems, program synthesis using ML, and program security. Readings include: formal methods and ML; robustness of neural networks and adversarial examples; verification and testing of neural networks and learning-based systems; neural techniques for program synthesis; verifying secure code.

Students are expected to lead in-class discussions and write an end-of-term paper (with extended literature survey and analysis) on a covered topic.

Sample reading list:
Seshia et al., Towards Verified Artificial Intelligence, 2016.
Katz et al., An Efficient SMT Solver for Verifying Deep Neural Networks, CAV 2017.
Huang et al., Safety Verification of Deep Neural Networks, CAV 2017.
Devlin et al., Neural Program Meta-Induction, NIPS 2017.
Almeida et al., Verifying constant-time implementations, USENIX 2016.

See instructor for complete list.

General Information

Location: Mon and Wed, 1:30--2:50 PM, CS Building 302

Professor: Aarti Gupta, CS Building 220, 258-8017, aartig@cs.princeton.edu

Office Hours: Mon and Fri 3:00--4:00 PM, CS Building 220

Graduate Coordinator: Nicki Gotsis, CS Building 310, 258-5387, ngotsis@cs.princeton.edu

Prerequisites: COS 510 or COS 516 (or, permission from instructor).

Resources

Reading List and Schedule

Shared on Google drive.

Announcements and Discussions
Course announcements, discussions, and questions: on Piazza.

Grading