Comp 681

Formal Methods

Spring 2019

Course Logistics

Blackboard: NC A&T uses the Blackboard course management system. You will find official announcements, course slides, additional lecture notes and practice programs on Blackboard. Blackboard is also where you will submit assignments.

Lectures: Lectures occur on T/R from 11:00am to 12:15 pm in McNair Hall 129

Textbook: Required readings are based on relevant textbook chapters as well as published research papers. There is not set required text.

Suggested Textbook: You may find the following textbooks of interest:

  • The Calculus of Computation: Decision Procedures with Applications to Verification by Aaron R. Bradley and Zohar Manna. ISBN:978-3-540-74113-8
  • Software Abstractions: Logic, Language, and Analysis by Daniel Jackson. ISBN:0262101149
  • Model Checking by Edmund M. Clarke, Orna Grumberg and Doron A. Peled. ISBN:0262032708

Course Description

Overview: The process of software validation includes reasoning about (the correctness of) programs, formally -- a process that is termed verification. A 2013 Cambridge study found software failures cost the world economy 312 billon dollars annually. This course is designed to explore formal methods as it relates to our ability to verify programs, designs and models. Learning the techniques and tools presented in this course is likely to significantly increase the students’ productivity as software developers and designers and improve the quality of the code they develop.
     The course content will cover techniques for theory, implementation, and applications of automated reasoning techniques, such as satisfiability solving, theorem proving, model checking, and symbolic execution. Topics include concepts from mathematical logic and applications of automated reasoning to the design, construction, and analysis of software.

Prerequisites: Graduate standing.

Policies

Grading: A student's grade in the class will be based on their performance on class participation, homework assignments, and a final semester project. The grade breakdown is: 3 homeworks worth 60% (20% each) and a course project worth 40% (5% project update, 15% in class presentation, and 20% final report).

Collaboration - Written homework: There will be three homework assignments given out over the course of the semester. Refer to the course calender for specific dates. These assignments are designed to give you hands on experience with the material presented in class. You may consult with classmates at a conceptual level, but the assignments are meant to be done individualy.

Use of Email: You cannot expect to get last-minute help on assignments by email. Although it's easy for you to dash off an email question, it takes time to answer it. In general, you should not ask email questions to which you can find the answer somewhere else (e.g., class notes, web page). If you must send an email, spend extra time to ensure that you are both brief and clear. Please include your name in the "From:" line of the email message, not just your email address. Email is a valuable tool for communicating with the instructional team. But be sure to use it properly, and follow the rules of good email etiquette (e.g., no flaming, spamming, etc.). Email messages will be sent to the student's A&T email address. It is the student's responsibility to regularly check their A&T email account.

Grade Disputes: If you are dissatisfied with a grade you receive, you must submit your complaint briefly in writing or by email, along with supporting evidence or arguments, within one week of the date that we first attempted to return the exam or assignment to you.
     The grade you are given on an exam, a quiz, an assignment, or as your final grade, is not the starting point of a negotiation. It is your grade unless a concrete error has been made. Do not come to the instructors or TAs to ask for a better grade because you want one or you feel you deserve it. Come only if you can document a specific error in grading or in recording your scores. Errors can certainly be made in grading, especially when many students are involved. But keep in mind that errors can be made either in your favor or not. So it is possible that if you ask to have a piece of work re-graded your grade will go down rather than up.
     Remember that the most important characteristic of any grading scheme is that it be fair. Keep this in mind if you're thinking of asking, for example, for more partial credit points on a problem. The important thing is not the exact number of points that were taken off for each kind of mistake. The important thing is that that number was the same for everyone.