Independent Study in Computer Science - Formal Verification
Table of Contents
Latest notes: Conclusion GitHub repo: https://github.com/selffins/lf
1. Information
Advisor: Giselle Reis (greis)
Student: (Earl) Louis Quilling (equillin)
Units: 12
Meets every Monday and Wednesday (except when noted) at 1008, 11:30 am.
2. Evaluation
2.1. Comprehension (60%)
Read the assigned chapter by the weekly meeting.
Create structured notes for concepts covered by the weekly meeting.
Attend the weekly meeting with the professor to discuss the chapter.
Reflect metacognitively about course progress and learning strategies and broader connections for each week.
2.2. Application (40%)
There are numerous book exercises. The goal is to complete a reasonable amount of exercises per chapter. There are “easy”, “medium”, “hard” problems – the student/teacher will set what “reasonable” means as the course progresses.
The student will aim to produce a verification of a program or mathematical theorem, but this is optional.
3. Learning Objectives
Learn to use the Coq Proof Assistant for mathematical assertions, mechanical checking, formal proofs, and extraction of certified programs.
Learn mathematical underpinnings of computer-assisted theorem proving, functional programming, operational semantics.
Learn to formally verify functional data structures/algorithms such as trees, maps, ordering, sorts, etc.
Learn to effectively communicate formal methods concepts.
Build strong habits and a decent familiarity for further in-depth study or research in formal methods.
4. Resources
4.1. Book https://softwarefoundations.cis.upenn.edu/
[./lf] - Logical Foundations
[./plf] - Programming Language Foundations
[./vfa] - Verifiable Functional Algorithms
4.3. Other
Types and Programming Languages, Benjamin Pierce
5. Topics
5.1. Logical Foundations (of Program Verification)
DONE Basics of Coq
DONE Proof by Induction
DONE Working with Structured Database
DONE Polymorphism and Higher-Order Functions
DONE Logic in Coq
DONE Inductively defined propositions
DONE Inductive principles
DONE Proof Objects
DONE Relations
DONE Maps
DONE Imp (skimming)
5.2. Programmming Language Foundations
DONE Program equivalence (skimming)
DONE STLC (skimming)
5.3. Miscellaneous
DONE Category theory + Logic + Type theory intro
DONE Research
DONE Conclusion
6. Schedule
| Week | Date | Content | Notes / Task | Meeting |
|---|---|---|---|---|
| Week 0 | January 9 | Intro | Syllabus | |
| Week 1 | January 13 | LF | Basics.v; Induction.v; | |
| Week 2 | January 20 | LF | Lists.v; Poly.v; | |
| Week 3 | January 27 | LF | Tactics.v; Research Presentation | |
| Week 4 | February 3 | LF | Logic.v; Research Proposal (CMU only) | |
| Week 5 | February 10 | LF | IndProp.v; | |
| Week 6 | February 17 | LF | ProofObjects.v; IndPrinciples.v | |
| Week 7 | February 24 | Break | ||
| Week 8 | March 3 | Misc | Category Theory (Aside) | |
| Week 9 | March 10 | Misc | Category Theory (Aside) | |
| Week 10 | March 17 | LF | Maps.v; Rel.v; | |
| Week 11 | March 24 | LF | Wrapping up LF | |
| Week 12 | March 31 | Break | ||
| Week 13 | April 7 | PLF | PLF skimming | |
| Week 14 | April 14 | PLF | Skimming Stlc | |
| Week 15 | April 21 | Misc | Proof Theory and Metacognition | |
| Week 16 | April 28 | Misc | Proof Theory | |
| Week 16 | May 1 | Misc | Conclusion |
7. Homework Submission
If you are using Software Foundations in a course, your instructor may use automatic scripts to help grade your homework assignments. In order for these scripts to work correctly (and ensure that you get full credit for your work!), please be careful to follow these rules:
Rules for Submission
- Do not change the names of exercises.
- Otherwise, the grading scripts will be unable to find your solution.
- Do not delete exercises.
- If you skip an exercise (e.g., because it is marked “optional,” or because you can’t solve it), it is OK to leave a partial proof in your
.vfile. - In this case, please make sure it ends with the keyword
Admitted(not, for example,Abort).
- If you skip an exercise (e.g., because it is marked “optional,” or because you can’t solve it), it is OK to leave a partial proof in your
- It is fine to use additional definitions (of helper functions, useful lemmas, etc.) in your solutions.
- You can put these before the theorem you are asked to prove.
- Handling Unproved Helper Lemmas
- If you introduce a helper lemma that you are unable to prove and end it with
Admitted, then make sure to also end the main theorem in which you use it withAdmitted, notQed. - This will help you get partial credit if you use that main theorem to solve a later exercise.
- If you introduce a helper lemma that you are unable to prove and end it with
Using Test Scripts
You will also notice that each chapter (like Basics.v) is accompanied by a test script (BasicsTest.v) that automatically calculates points for the finished homework problems in the chapter. These scripts are mostly for the auto-grading tools, but you may also want to use them to double-check that your file is well formatted before handing it in.
Testing in the Terminal
In a terminal window, either type:
make BasicsTest.vo
Or, do the following:
coqc -Q . LF Basics.v coqc -Q . LF BasicsTest.v
8. Directory
Each directory contains .v files and .html files. The important ones in each directory are:
Preface.v or Preface.html
The place to start reading, including details on how to install required software
index.html
The book’s cover page and navigation starting point
deps.html
Overview of the ordering of chapters
9. Health and Wellbeing
The student is required to prioritize their wellbeing and seek assistance if problems are encountered.