Princeton University
Computer Science Department

COS 598B: Advanced Topics in Computer Science
Advances in Automated Reasoning

Aarti Gupta

Spring 2020

Course Description

This seminar explores recent research advances in automated reasoning that tackle logic-based problems beyond satisfiability - model counting, optimization modulo theories, and automated synthesis. We study recent papers that cover core techniques and their applications in reasoning about quantitative properties (e.g., in security, fairness, optimization for resources).

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:
Albarghouthi et al., FairSquare: probabilistic verification of program fairness, PACMPL 1(OOPSLA) 2017.
Biondi et al., Scalable approximation of quantitative information flow in programs, VMCAI 2015.
Chakraborty et al., Distribution-aware sampling and weighted model counting for SAT, AAAI 2014.
Fredrikson et al., Satisfiability modulo counting: a new approach for analyzing privacy properties, CSL-LICS 2014.
Knoth et al., Resource-guided program synthesis, PLDI 2019.
Smith et al., Synthesizing differentially private programs, PACMPL 3(ICFP) 2019.

Please see instructor for complete list.

General Information

Location: Mon and Wed, 11:00--12:20 PM, CS Building 302

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

Office Hours: by appointment.

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