- Final Exam
- Final Errata 1
- Lecture Notes April 14
- Lecture Notes April 12
- Pset16 Update
- No Class April 5
- Next Up
- Lecture Notes Feb 15
- Lecture Notes Feb 10
- Lecture Notes Feb 08

Blog

Software Requirements Modeling and Analysis is an advanced introduction to modern techniques for specification, verification and implementation of computer-based systems. Students will learn to write formal specifications, refine specifications and verify that implementations meet their requirements. Specific topics include axiomatic specification, invariants, algebraic types and induction, constructive specification, assume-guarantees style specification, safety and liveness, and intuitionistic logic. We use the Coq proof system, but techniques learned apply equally well to other verification systems.

- Room and Time
- 2112 Learned Hall
- 2:30-3:45 TR
- Prerequisites
- Some discrete mathematics and functional programming.
- Instructor Information
- Dr. Perry Alexander
- Office Hours: 1:30-2:30 TR in 3048 Eaton Hall, or by appointment
- Office: 3048 Eaton Hall / 208 Nichols Hall
- Phone: 4-7741
- Web: https://perry.alexander.name
- Email: palexand@ku.edu
- Textbooks
- Adam Chlipala,
*Formal Reasoning About Programs*, published online (required) - Benjamin Pierce,
*Software Foundations*,published online (required) - Resources
- Coq proof system.
- CoqIDE if you don’t want to use emacs.
- VScode is an even better option if you don’t want to use emacs. Coq integration is available, but you will still need to install Coq on your machine.
- ProofGeneral if you do want to use emacs. ProofGeneral is also available via melpa if you prefer not to install by hand.
- Chlipala’s Coq Quick Reference is a pretty good summary of commands we’ll use.

`git@github.com:ku-sldg/eecs755-public.git`

- Solutions
to assignments and other materials that need to remain private. If
you wish to have access to this private repo, send email to the
instructor with your GitHub ID. Do not post anything in this repo
publicly! Adam Chlipala has done us a great service by making his
materials public. Please respect that by not posting solutions to
his problem sets.

A few definitions from my notes that I feel are important:

**Proof State** - The proof you are currently working on. Commands
entered operate on the proof state. Some change it. Some do not.

**Goal Stack** - The proofs you still need to do. Literally in a stack.

**Decision Procedure** - a routine for determining if a logical term
is `true`

or `false`

. Always terminates. Never changes the proof
state.

The FRAP book does a nice job of defining each command when it is first used. In this list I’m identifying the proof tactics that we’ve used in class. See the book for more complete definitions.

`simplify`

- basic simplification and evaluation.`induct v`

- perform induction on`v`

. Produces new proof goals for each inductive case.`equality`

- decision procedure for equality terms`linear_arithmetic`

- decision procedure for systems of inequalities.`unfold n`

- replace`n`

with its definition. Add a`*`

to unfold everywhere. Add a term name to unfold in just that term.`case x`

- perform a proof-by-cases on possible values of`x`

.

`Definition`

- define a non-recursive structure`Inductive`

- define an inductive type`Fixpoint`

- define a recursive function`Theorem`

or`Lemma`

- Define a new theorem or lemma to prove. Usually followed by`Proof`

`Proof`

- enter the proof scripting engine`Qed`

- Done. End of a proof scripting session. Quick Eat Donuts.`Module M.`

…`End M.`

- Open and close a module named`M`

.

- Homework 1 - Due: February 4 11:59pm

- Midterm Exam - Date: March 31, during class

You will perform several projects that involve developing specifications and proofs using the Coq verification system. These projects are an exceptionally important part of the course and provide insight into writing and verifying specifications and code that cannot be gained by simply attending lectures. Verification projects will be assigned every 1-2 weeks.

Please use KU’s Canvas system for project submissions. Your
specification files should be self-contained including any
needed documentation. `coqdoc`

is a great way to document your
specifications, but is not required.

All exams are closed book, closed notes, in-class exams. The final exam will be held during the time assigned by the University in our regular classroom.

Grades are assigned on a standard 10 point scale:

- A = 90-100%
- B = 80-90%
- C = 70-80%
- F = 0-60%

I do not use +/- grading scale. As this is a graduate class, the lowest passing grade is a C.

Classroom tasks are weighted using the following scale:

- Midterm Exam 30%
- Final Exam 30%
- Mini Projects 40%

You must pass both mini projects and exams separately to pass the class. Specifically, if you get less than 60% on your projects and homework or less than 60% on your exams, you will not pass the course.

I may curve final grades at the end of the semester. However, I will never curve individual assignments or exams. If I curve and how much I curve is at my discretion.

Pretty simple. Follow them and we’ll be great friends!

- Don’t whine
- Don’t cheat
- Be kind

I do not take attendance in class, however participation in class is important to its success. How much homework and how rigorously it is graded will definitely depend on class participation. Please ask questions and participate in class discussions. When assigning final grades, borderline cases will be decided based on class participation.

If I have made an error in grading an exam or assignment, you have two weeks following the date the item is available to see me about correcting the problem. Note that this includes the final! After that time, your grade is set and will not be changed. I also request that you wait 24 hours after an exam is returned before coming to me with questions.

I may decide to curve final scores when the semester is over. Whether I curve and how much I curve is at my discretion. I will never curve up, but may curve down. Specifically, 90% and above will always be an “A”, but I may choose to lower the cutoff percentage. Whether I curve and how much I curve is at my discretion. I will never curve scores on an individual graded assignment or exam.

I encourage you to use email to contact me. I am logged in whenever I am working and check my mail frequently. Email is my preferred means of communication.__

The course blog is available on the website. I will post late-breaking news about projects, homework and class administration on the blog. Check the website and blog frequently, particularly around project due dates and exams.

Feel free to call me in any of my office at any time. I would prefer not to be called at home.

I will make every effort to be in my office during scheduled office hours. If there are exceptions, I will let you know as early as is possible. If you have a conflict with my office hours, please make an appointment. I have an open door policy, you are free to come by whenever you choose. If I am busy, I may ask that you come back later, but please don’t hesitate to ask!

Academic misconduct of any kind will automatically result in a 0 score on the homework, lab, project, or exam in question and your actions will be reported to the department chair. Your homework, exams and projects must be individually prepared unless otherwise noted. Posting your assignments to internet discussion lists is considered academic misconduct. Sharing your solutions with others is considered academic misconduct. Turning in solutions from previous semesters is considered academic misconduct. Paying people to prepare solutions is academic misconduct. Automated mechanisms are available for checking the originality of source code. Please spend your time trying to solve assigned problems rather than trying to get around the system. Don’t risk it!

Excusing a missed exam or assignment is left to my discretion. Illness, family emergencies, and religious observances are examples of acceptable excuses. Computer down time, over sleeping, and social events are examples of unacceptable excuses. Please try to let me know of problems in advance when possible and be prepared to provide verification of your excuse.

As a policy, I do not extend due dates of homework and projects. If I choose to do so, I will only announce the extension in class, via email or on the blog. If you hear an extension has been granted and I have not announced it, your information is incorrect. Remember that if I grant extensions early in the semester, it will necessarily compress due dates the end of the semester.

We will do quite a bit of bouncing around between topics and between our two texts. It is quite important that you be in class. I will also add miscellaneous topics throughout the semester. Specific topics are subject to change without notice and topics marked “(tentative)” will be covered as time permits.

- Formal Systems
- Introduction to Coq
- Concrete and Abstract Syntax
- Inductive Types
- Constructive Specification
- Interpreters
- Transition Systems and Invariants
- Assume-Guarantee Reasoning
- Model Checking
- Safety and Liveness
- Compiler Verification
- Operational Semantics
- Dependent Types (tentative)
- Curry-Howard Correspondence (tentative)
- Proofs and Proof Objects (tentative)
- Proof Tactics and Tacticals (tentative)