- Midterm Clarification
- Midterm Exam
- Midterm Exam Info
- Classes Fall 24
- Tactics So Far
- Homework Grading
- Basics Updated
- Welcome

Blog

Software 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 verification, 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
- 1136 Learned Hall
- 2:30-3:45 TR
- Prerequisites
- Some discrete mathematics and functional programming.
- Instructor Information
- Dr. Perry Alexander
- Office Hours: 3:45-5:00 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
- Benjamin Pierce, et. al.,
*Logical Foundations - Software Foundations Volume 1*, published online (required) - Benjamin Pierce, et. al.,
*Programming Langauge Foundations - Software Foundations Volume 2*, published online (required) - Adam Chlipala,
*Formal Reasoning About Programs*, 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.
- ProofGeneral if you do want to use emacs. ProofGeneral is also available via melpa if you prefer not to install by hand.

Please submit your assignments on the class Canvas Site.

- 1/18 Course introduction and Gallina basics
- Lecture: Introduction, Basics
- Album:
*Aja*, Steely Dan - 1/23 Gallina basics
- Lecture: Basics
- Album:
*Aging*, Kevin Drew - 1/25 Gallina basics
- Lecture: Basics
- Album:
*Let’s Face It*, The Mighty Mighty Bosstones - 1/30 Proof by induction
- Lecture: Induction
- Homework: Basics.v, BasicsTest.v
- Album:
*Legacy: The Instrumental Jawn*, Adam Blackstone - 2/1 Proof by induction
- Lecture: Induction
- Album:
*1972*, Josh Rouse - 2/6 Structured Data
- Lecture: Lists
- Homework: Induction.v, InductionTest.v with two 3 star or above problems.
- Album:
*The Omnichord Real Book*, Meshell Ndegeocello - 2/8 Structured Data, Polymorphism
- Lecture: Lists, Poly
- Album:
*The Room*, Sam Gendel and Fabiano Do Nascimento - 2/13 Proof Tactics
- Lecture: Tactics
- Homework: Lists.v, ListsTest.v with two 3 star or above problems.
- Album:
*Nothing’s Shocking*, Jane’s Addition - 2/15 Proof Tactics
- Lecture: Tactics, Logic
- Album:
*Bright Size Life*, Pat Metheny - 2/20 Logic
- Lecture: Logic
- Homework: Poly.v, PolyTest.v with two 3 star or above problems. Tactics.v, TacticsTest.v with two 3 star or above problems.
- Album:
*Featherweight*, Rosie Frater-Taylor - 2/22 Logic in Coq and Inductive Propositions
- Lecture: Logic, Inductive Propositions
- Album:
*Psychadelic Backfire II*, Elephant9 with Reine Fiske - Midterm Topics Stop Here
- Specific study topics are listed below
- 2/27 Inductive Propositions
- Lecture: Inductive Propositions
- Homework: Logic.v, LogicTest.v with two 3 star or above problems.
- Album:
- 2/29 Inductive Propositions and Proof Objects
- Lecture: Inductive Propositions, Proof Objects,
- Album:
- 3/5 Maps and Imp
- Lecture: Maps, Imp,
- Album:
*Can You Hear It?*, Innanen, Pasborg, Piromalli

- Midterm Exam - Date: March 28

You will perform homework that involves developing specifications and proofs using the Coq verification system. These assignments 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. Homework will be assigned every week with the exception of exam weeks.

Each homework problem is assigned points by its number of stars as follows:

- 1 star = 1 point
- 2 stars = 2 points
- 3 stars = 3 points
- 4 stars = 5 points
- 5 stars = 10 points

Total points for an assigned homework file is the sum of all problems in the file. Total grade points is 2/3 of the available points rounded up. Thus, your goal is to complete 2/3 of the points available in a file. If you do more, you will receive extra credit for 1/3 work beyond the 2/3 goal. For each homework you will also be asked to do a minimum of 3 and 4 star problems.

For example, if there are 35 points available for an assignment, your goal is 23 points. I may also separately require one or more 3 or 4 star problems as a part of your total. Extra credit is calculated as ((file total - 23)/3) if (file total - 23) is not negative.

All assignments assigned prior to the midterm will be due before the midterm. All assignments prior to the final will be due before the final. Do not wait until the last minute. Individual due dates are provided to help you keep pace with the class and represent the earliest I will start grading. If I suspect the class is not keeping up, I will enforce hard due dates.

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%
- Homeworks 40%

You must pass both mini projects and exams separately to pass the class. Specifically, if you get less than 60% on your homeworks 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

**Class Participation** - 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.

**Grading Errors** - 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.

**Curving** - 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.

**Email** - 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.__

**Blog** - 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.

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

**Office Hours** - 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.

**Cheating** - 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!

**Exceptions** -
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.

**Extensions** - 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 three texts. It is quite important that you be in class. We will
start in *Logical Foundations* and follow the recommended path
for a semester course. We will them move to *Programming Language
Foundations* and again follow the recommended path for a semester
course with several topics on program verification from
*Formal Reasoning About Programs*.

- Introduction to Coq
- Inductive Types
- Structured Data
- Polymophism and Higher-Order Functions
- Logic
- Inductive Propositions
- Total and Partial Maps
- Imperative Programs
- Program Equivalence
- Transition Systems and Invariants
- Safety and Liveness
- Model Checking
- Operational Semantics
- Type Checking (tentative)
- Compiler Verification (tentative)
- Assume-Guarantee Reasoning (tentative)