Computational Logic and Software Verification

The goal of the written homework is to help you refine the fundamental skills, and better understand the theoretical underpinnings, that you will need in order to do well on the labs and exams. Grading for these assignments is based on the correctness of your answer, and the presentation of your reasoning. You should strive for clarity and conciseness, while making sure to show each step of your reasoning. Categorical answers with no explanation will not even receive partial credit, but lucid explanations of your attempt to find the answer will.

Written homework will be handed in in PDF format via teams, and should preferably be typeset in LaTeX.

The programming homework is designed to give you hands-on experience writing bug-free code with the help of formal verification tools. In general, we will ask you to implement some interesting functionality, such as a SAT solver or fault-tolerant communication protocol. The most important criterion with respect to grading programs is correctness.

Programming Homework will be send in a Unix compressed archive name.tgz. Your archive must include a README file describing how to compile and run your program. It must also include a short report (2 pages max.) describing the salient parts of your code.

Students are expected to complete each assignment on their own, and should be able to explain all of the work that they hand in. Copying code or proof material from other students, from online sources, or from prior instances of this course is not allowed. However, you are encouraged to discuss assignments with each other at a sufficiently high level to avoid the risk of duplicating implementation or proof. Examples of this would be discussing algorithms and properties referred to in the assignment, helping other students with questions about a programming language or tool required to complete the assignment, discussing a general proof technique, or referring to an online source with useful information. Similarly, you may consult online sources, tutorials, and public libraries. If you find specifically helpful material it is critical that you (a) do not copy the code or proof, but study it as a guide and then do your own work, and (b) cite the source with your classmates' names, suitable URLs and chat prompts (if you use any generative AIs) in your solution. If you have questions about whether something might be permissible, contact the course staff before you proceed.