Logic for Systems

“What do you want?”

This question is perilous, yet indispensable in life. And it remains vital in designing, understanding, and building systems. How will you check that you’ve achieved your goal? What is the cost, and which assumptions are you making along the way? Do you really want what you think you do, and will your code (or other artifact) actually work?

These questions matter, whether you’re crafting a new data structure, finishing up a programming assignment, designing a processor, or arguing over the rules of Monopoly with your family. In this course, you’ll use concrete software tools (e.g., model checkers and SAT solvers) to bring the power of automated reasoning to bear on these and other quandaries in, and outside of, computer science.

Logic for Systems is built on three broad learning categories:

• modeling systems and making good abstraction choices;
• reasoning about systems automatically using logic; and
• the foundational algorithms behind the tools used both in this class and in industry.

The course culminates in a student-proposed, staff-mentored project that applies to a real-world system. Past projects have involved everything from distributed hash-tables to baseball games. Prerequisite: CSCI 0160, CSCI 0180, CSCI 0190, or CSCI0200.

The course syllabus contains important information regarding attendance expectations and academic integrity.

If you’re unsure about whether this is the right course for you check out our FAQ!