CIS 301, Logical Foundations of Programming, Fall 2019


Summary

This course teaches the fundamentals of symbolic logic: how to write proofs, and how to reason semantically. The acquired techniques will be used for the reasoning about program behavior.

Logistics

Personnel

Schedule

EventPlaceMondayTuesday WednesdayThursdayFriday
ClassesDurland
1073
9:30-
10:45am
9:30-
10:45am
Torben
Office Hours
Engineering
2179
1-2pm 2-3pm 3-4pm
Bud
Office Hours
Engineering
1117
1-2pm 4-5pm
in 1116
8:30-9:30am
Sarthak
Office Hours
Engineering
1116
3:30-4:30pm 3:30-4:30pm 3:30-4:30pm

Communication

Use the email address help-301@santoslab.org for all questions about lectures, homework, and appointments. Do not email the TAs or instructor directly (unless there is a very good reason), and do not use Canvas messaging to contact us.

We make efforts to keep up with email (even though we may not check our inboxes all the time), and it is our goal that you should expect an email answer no later than on the next business day. So if you send an email on Friday, we will aim to get back to you the next day the university holds classes (which will typically be Monday), and often even earlier.

For questions (or comments) of general interest, we encourage that you post in the Canvas discussion forum so that also other students will benefit from the answers. We even encourage you to answer questions from other students (of course you should not give more hints towards solutions than you would reasonably expect the instructor to give).

Course Material

Course Notes

The main course material is the notes Logika: Programming Logics, available at http://logika.sireum.org/dschmidt/ and developed by David Schmidt, later modified by Bud LaVezzi and John Hatcliff.

Other references may be provided as the course unfolds.

Software Tools

The main tool is Sireum Logika, available at http://logika.sireum.org and developed by Robby.

Logika is a program verifier and a natural deduction proof checker for propositional, predicate, and programming logics. Logika is part of a much larger analysis and verification framework, called Sireum, developed by Robby.

It is crucial that you get set up to use Logika during the first week of class. We will use Logika every week in class, and almost all homework assignments will use it.

Logika can be used in a nice IntelliJ-based Integrated Verification Environment (Sireum/Logika IVE); this is what we recommend for doing all your classroom exercises and homework.

Objective and Topics

The first notions of formal logic were invented over 2000 years ago as philosophers attempted to develop systematic approaches for arriving at statements that were true. By the time we approach adulthood, we will have heard many people say (or we will have said ourselves): that seems logical, or you're being illogical. By this, we understand that (in the first case) sound reasoning principles have been used, whereas in the latter case someone may be stating a conclusion that cannot be justified by sound reasoning from an initial set of true facts. This "every day" notion of logic that manifests itself in the arguments that we make in natural language is sometimes referred to as informal logic.

In contrast, in this course, we will study concepts related to formal logics. In simple terms, a formal logic consists of some syntax for stating claims (properties that are either true or false) about the world (or some other more specialized domain in which we are interested), and rules for deriving claims that are guaranteed true.

Formal logic is deeply tied to computer science, because computers are great at "blindly following rules", and many interesting issues in computer science can be phrased as basic claims together with systems of rules. Formal logics can define and explain, for example, the basic gates and circuits from which computers are built, the behavior of our programs as they execute, the protocols that our computer systems use to communicate, the expert systems that provide automated assistance to professionals such as doctors or pilots. Formal logic thus provides, which is very important, the basis for automated rule-based reasoning for these systems.

In this course, we will learn the basic elements found in a formal logic, including syntax for claims and rules for making deductions. We will also learn how to judge if our rules are suitable in the sense that they only lead us to claims that match the reality of the domain we are reasoning about.

Our focus will be on formal logics for reasoning about program behavior and for programming directly in terms of logic. We will see how tools based on logic are used to reason about safety and security critical software, network security, and security protocols.

Grading

Final letter grades are not based on strict percentage cutoffs but are "curved" by taking into account the difficulty of the exercises and exams. As a rule of thumb, however, you should expect that it requires almost 90 % to earn an A, a bit above 75 % to earn a B, and somewhat more than 60 % to earn a C.

In general, my approach to grading is expressed well by this piece by S.A. Miller.

Homeworks

are due most weeks and are to be submitted through Canvas.

Exams

will be closed-book and closed notes. The final will be comprehensive, but with emphasis on the latter part of the course.

Grievances

If you think the instructor or the TAs have made an error when grading your test or your homework, you are of course very welcome to ask for clarification. But complaints about judgment calls, like how much credit to give for a partially correct solution, are not encouraged (it is like arguing balls and strikes).

Academic Honesty

Kansas State University has an Honor and Integrity System based on personal integrity, which is presumed to be sufficient assurance that, in academic matters, one's work is performed honestly and without unauthorized assistance. Undergraduate and graduate students, by registration, acknowledge the jurisdiction of the Honor and Integrity System. The policies and procedures of the Honor and Integrity System apply to all full and part-time students enrolled in undergraduate and graduate courses on-campus, off-campus, and via distance learning. A component vital to the Honor and Integrity System is the inclusion of the Honor Pledge which applies to all assignments, examinations, or other course work undertaken by students. The Honor Pledge is implied, whether or not it is stated: "On my honor, as a student, I have neither given nor received unauthorized aid on this academic work." A grade of XF can result from a breach of academic honesty. The F indicates failure in the course; the X indicates the reason is an Honor Pledge violation.

You are very welcome to discuss the course material, as well as specific questions, with your fellow students. However, all submitted answers must be your own work:

If you are in doubt about what is permissible, please ask me. I very much hope that it will not be necessary to file any honor pledge violation reports during the semester!

Other Administrative Issues

Acknowledgments

Most of the course material, including much of this syllabus, is adapted from previous courses taught by John Hatcliff and Robby and (less recently) David Schmidt (the original creator of the lecture notes) and Torben Amtoft.


Torben Amtoft