Frequently Asked Questions (FAQ) and their answers

General Course Info is in Section 7

1  Online Material

Lec1, 1/9/12:

• Lec1 slides
• Background Quiz

Lec2, 1/11/12:

• Lecture 2 notes PLUS Assignment 1, [.pdf] [.tex]

Lec3, 1/18/12:

• Assignment 2 Solution
• Lecture 3 notes PLUS Assignment 2, [.pdf]
• TR on the GRASP SAT solver
• An Ocaml book by Jason Hickey
• Some Python notes - see embedded references in these notes, as well
• Chapter 18 of my book
• PySat.tar.gz is here. To use it, you can get on any machine that has Python3, or for now, simply ssh into lab3-20 (say). Then cd ~cs6100/public_html/PySat/tests/ and then type ./testfile.py TestFiles/sat2.cnf (for instance) . For more details, see the README there. (I had to copy over argparse.py into the tests directory. I did not come as a default on the lab3 machine. It seems to work.)
• cnf.ml is here

Lec4, 1/23/12:

• Lecture 4 notes [.tex] from which you can get embedded Python codes, if you wish.

Lec5, 1/25/12:

• Krstic’s paper on SAT/SMT through a transition system
• User manual of the DPvis tool (thanks to Carsten Sinz)
• Survey of SAT, circa 1990s by Jun Gu

  Also in PDF

• Part of today’s notes in .txt

Lec6 and Lec7, (1/30 and 1/2, 2012:

• Assignment 3 [.pdf] – [.tex] – given 2/1/12, due 11:59 hrs, 2/8/12.
• Andersson’s BDD notes covering combinational and sequential verification
• Tyler’s Python BDD package following Andersson’s BDD notes
• Filliatre’s Ocaml BDD Package - worked out of the box for me
• My BDD notes, including encoding of Puzzles
• A Minimized Automaton Representation of Reachable States, by Holzmann and Puri
• Knuth’s BDD chapter
• Knuth’s video lecture on BDDs
• Bryant’s posting on Knuth’s BDD work
• Adnan Aziz’s slides - look for the ones on BDDs

Lec8 and Lec9 (2/6 2/8, 2012):

• notes8.[.pdf] [.tex]
• review.[.pdf] [.tex]
• asg4.[.pdf] [.tex]
• MyBook [.pdf]

Lec10 and Lec11 (2/13-15, 2012):

• notes10.[.pdf] [.tex]
• Jason Cantin’s proof that checking coherence is NP-complete[.pdf]

Lec12, (2/22, 2012):

• Jason Cantin’s MS thesis which has more details: [.pdf]
• Encoding of the SAT and UNSAT examples from Cantin’s thesis using MPEC is here as a [.txt] file. Note: if you have to install MPEC, you may need to update some C++ libraries (follow install messages).
• Assignment 5, and Notes for Lecture 12. This assignment is due 2/24 and 3/2 (in two installments).

Checklist for 2/24/12:

• Assignment 5: 2/24 and 3/2 (two submissions), and Notes 12: I suggest that you bring a copy of notes12.pdf (see under Lec12, 2/22) to class
• Project group info, project topic (if known): send by 2/24/12
• Project topic selection to be finalized—project proposal (1 page) due 3/9/12
• Readings for 2/27 and 2/29 (see above)

Lec13 (2/27)

• Reading for 2/27: A Minimized Automaton Representation of Reachable States, by Holzmann and Puri
  • Wei-Fan’s lecture on this topic on 2/27 [in PDF]

Lec14 (2/29)

• Reading for 2/29:
• Path to z3 (you may download, but a Linux binary is kept at): /home/cs6100/bin/z3
• Reading for 2/29: Z3 Tutorial[.pdf]
• Reading for 2/29: Z3 Sampler[.pdf]
• Tyler’s lecture on this topic on 2/29 [in PPT], and [in PDF]

Lec15 (3/5)

Invariant generation, Z3, First-Order Logic (FOL).

Assignment 6 given on 3/5. DUE 3/19/12. Assignment in [.pdf] and in [.tex], with Sample Solutions

Slides for 3/5 are here: in [.pptx] and in [.pdf]

Lec16 (3/7)

Lecture by Sriram on using invariants for enhancing system resilience

Lec17 (3/19)

Lecture by Ganesh – SLIDES are in in [.pptx] and in [.pdf]

Lec18 (3/21)

Lecture + problem-set + Prenexing in Ocaml: Notes in [.pdf]

Lec19 (3/26)

Lecture on the Undecidability of the Validity of First-Order Logic in [.pdf]

Lec20 (3/28)

Midterm exam [.pdf] and its solution Midterm exam [.pdf]

Lec21 (4/2)

Presburger Overview + Ch-3 of B/M Papers on Presburger Reasoning and Applications

and there are notes kept at: notes21.pdf

Lec22 (4/4)

Assignment 7 in [.pdf]

Lec23 (4/9)

• Notes discussed in class on Monday 4/9/12
• The original paper on subgoal induction by Morris and Wegbreit - [.pdf]

Course notes from a course offered at Intel in year 2000. Pay attention to the following intel-verification-course

• The subgoal induction method presented in notes.pdf in this directory
• A subgoal induction prover written by a student (Sid Bytheway) in this directory
• We will study how to verify a pattern matcher and a topological sorting program - listed in this directory - using subgoal

Lec24 (4/11)

Even though I have argued topsort correct in intel-verification-course, I clean up a bit and present it again.

Contents

• 1  Online Material
• 2  About the Course
• 3  Class Requirements
• 4  Course Plans
• 5  Project Topics
• 6  Reference Materials
• 7  General Course Info
• 8  Holidays etc.
• 9  HANDOUTS AND WEEKLY SCHEDULE
• 10  Policy Statement of Academic Misconduct
• 11  Students with Disabilities

2  About the Course

This course ¹is meant for graduate and advanced undergraduate students (unless otherwise allowed by the instructor).

The topics selected for the Spring 2012 offering are the following:

• Mathematical logic, emphasizing the use of decision procedures (satisfiability modulo theories)
• Concurrency, emphasizing basic model checking and shared memory consistency models
• Specifying systems, emphasizing Operational Semantics.

These topics are intimately related, and all pertain to one’s ability to understand and design correctly functioning systems, and describe the workings of these systems clearly. The onus is on you (the student) to develop a clear understanding of what the course is about, and how you can best tailor the course (influence what will be lectured, and negotiate degrees of freedom that you are comfortable with) to maximize your learning. Please bear in mind that

• This is a required class, and hence I have to make sure that certain basic topics have been learned, and best practices have been created; yet
• You all have widely different backgrounds, and so I also have to make sure that I stay out of your way whenever possible, letting you pursue topics with the required degree of commitment; also
• Working all by yourself, and showing something fantastic in code-form during the last week is not going to serve the interests of this course. You should maximize your opportunities to teach the rest of the class and the instructor about things you discover, so that we all learn more about topics that cannot be discussed in class. This will be achieved if you participate in class discussions, discussions with the instructor during office hours or during class, talking to classmates, and participating in classroom presentations of your project.

3  Class Requirements

This is a project-based class. Attendance to the lectures is required, unless you excuse yourself through an explicit email before the lecture begins. A formal roll-call will not be taken; however, prolonged absences without a reason will be grounds for failure.

4  Course Plans

Interactions during lectures or through email will earn you participation points (10% of the course grade). There will be one midterm (20% of the course grade). The rest of the course grade is based on assignments (20%) and a project (50% of the course grade). The final grading will be based on a curve, typically with each percentile of 10 binned into a grade category (e.g., 90-100: A, 80-19: B, etc.)

The projects are meant to be done either individually or in groups of size 2 (if there is a very well motivated reason for a group-size of 3, that may be permitted). There will be a required project presentation during the last week of classes. Points toward your project will be assigned based on the quality/novelty of the work itself, your presentation, and your report. Projects are required to be selected during the first two weeks of classes, from the list of topics given in Section 5 (to be refined soon; these are general topics for now).

There will be 1-1 project meetings held during the third week of classes. Changes in project focus/topic can be negotiated during these meetings. Generally, these meetings will be scheduled to occur during office hours; however, lecture-time may also be set apart.

Proper citations are expected whenever external public-source material is referred to. Help from your classmates or friends is allowed to the extent that it teaches you the basic methods/approach – and it must be acknowledged in your presentations, assignments, etc. All the worked turned in must be original. In particular, for specific problems assigned, and unless otherwise specified, you must be solely responsible for the creation of the actual solution, code module, etc.

5  Project Topics

• Using SMT solvers for
  • Test generation
  • Code generation
• Writing shared memory consistency specifications for
  • Machines
  • Languages
• Applications of course topics to program/model/protocol analysis, including in computer security and emerging domains

6  Reference Materials

The course will be based on lecture notes, and the references below:

• A book by Bradley and Manna. Since we will be covering only four chapters, you don’t need to purchase a copy; instead you may follow this link to access its PDF: http://www.springerlink.com/content/wv0127/#section=311472&page=1
• Two references for the topic of shared memory consistency models are a book by Hill et al. and a PhD dissertation by Sevcik.
• A good set of references on Operational Semantic specifications is the work by Rosu and his team at UIUC. Look at the K/Matching Logic website for papers and tools. This material will complement our discussion of concurrency.
• You will also find an excellent set of notes courtesy of Dr. Konrad Slind at http://www.eng.utah.edu/~cs3100/KonradNotes.pdf that gives crystal-clear explanations of many theoretical concepts. This material is typically covered in CS 3100 whose website can also prove handy.

7  General Course Info

• Class Website: http://www.eng.utah.edu/~cs6100
• Class Room: MEB 2475
• Lecture Hours: MW 11:50 to 13:10
• Instructor: Ganesh Gopalakrishnan
• Instructor Email: My CS Email with a subject beginning with “cs6100”.
• Instructor Office Hours: Mon : 14:00 to 15:20 and Tue : 15:00 to 16:30
• Instructor Office Location: 3428 MEB

8  Holidays etc.

My known commitments are below. Some of these days, classes may actually be held (so don’t assume an automatic “no class” unless it is a holiday).

• January 16 : Martin Luther King Day holiday
• February 20 : President’s Day holiday
• February 25 - 29 : PPoPP (New Orleans)
• March 5-7 : At NSF (panel)
• March 12-17 : Spring break
• Apr 17, Tue, 10:15am - earthquake drill (FEMA)

9  HANDOUTS AND WEEKLY SCHEDULE

• Week1
  • 1/9/12 L1: Introduction to the course

10  Policy Statement of Academic Misconduct

A link to the SoC Policy Statement of Academic Misconduct appears at:

http://www.cs.utah.edu/internal/cheating_policy.pdf.

If you have not done so, please read the above policy, print the following acknowledgement form, sign it, and hand it over to the SoC office or me:

http://www.cs.utah.edu/internal/SoC_ack_form.pdf

11  Students with Disabilities

Reasonable accommodation will gladly be provided to the known disabilities of students in the class. Please let the instructor know the situation as soon as possible. If you wish to qualify for exemptions under the Americans with Disabilities Act (ADA), you should also notify the Center for Disabled Students Services, 160 Union Building.

1

I frankly don’t care whether you register for 5100 or 6100; do what the system readily allows you to - except grad students are normally expected to register for 6100, given a choice.

This document was translated from L^AT_EX by H^EV^EA.