Software Modeling and Analysis is an advanced introduction to formal methods including 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-guarantee style specification, safety and liveness, and intuitionistic logic. Students will also learn techniques for employing LLMs in the verification process.
Please submit your assignments on the class Canvas Site.
You will perform homework that involves developing specifications and proofs using the Rocq 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 except for exam weeks.
Each homework problem is assigned points by its number of stars as follows:
Total points for an assigned homework file is the sum of all problems in the file. Total grade points is 3/4 of the available points rounded up. Thus, your goal is to complete 3/4 of the points available in a file. If you do more, you will receive extra homework credit for 1/4 work beyond the 3/4 goal. However, you will not receive more than 100% for the semester. 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 26 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 - 26)/4) if (file total - 26) 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 “bring back” exams. You will be given a copy of the exam one class period before the exam is due. You can do anything you want to prepare for the exam. When you come to the next class you will be given a blank exam that you will complete closed book, closed notes in class. 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:
I do not use a +/- grading scale. As this is a graduate class, the lowest passing grade is a C.
Classroom tasks are weighted using the following scale:
You must pass both homework and exams separately to pass the class. Specifically, if you get less than 60% on your homework or less than 60% on your exams, you will not pass.
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!
Class Participation - I do not take attendance; 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.
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.
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.
AI - I encourage you to use AI in preparing your assignments under the following guidelines. Using AI for proofing and cleaning up solutions is appropriate without citation. Using generative AI to assist with proving or specification or generating text is also appropriate when it is properly acknowledged, and your prompts are included as a part of your solution. Using generative AI without proper attribution is claiming work you did not do and is considered academic misconduct. If you use AI tools simply document what you did.
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 downtime, oversleeping, 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 at 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 then 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.