CS 6110 – Formal Methods in System Design – Spring 2011Ganesh Gopalakrishnan |
You are required to read the indicated chapters ahead of time, at least cursorily, to get an idea of what will be covered.
In lieu of physical 1-1s, I am expecting an email from each project group, so that I can lecture on SMT solvers. In this email, I am expecting:
| Date | Event |
| 3/17 | Project group 1-1 meetings - see § 3.2 |
| 3/29 | Lecture on SMT solving (Yices, Z3) |
| 3/31 | Project group 1-1 meetings - see § 3.2 |
| 4/5 | Ganesh away 4/5-4/14 on two trips: Email appointments with Greg |
| 4/7 | Project group 1-1 meetings with Greg - see § 3.2 |
| 4/12 | Ganesh away - Email for appointments with Greg |
| 4/14 | Project group 1-1 meetings with Greg - see § 3.2 |
| 4/19 | Lecture |
| 4/21 | Project group 1-1 meetings - see § 3.2 |
| 4/26 | Final Project Presentations. See § 3.3. |
| 5/5 | Final Project Reports due. See § 3.4. |
I am allowing 5 mins for 1-person projects, 7 mins for 2-person projects, and 9 mins for 3-person projects. The project meetings will be held in our class room (LCR) itself. The projects and the students are as follows.
By the midnight of 3/17/11, each group is required to send me two URLs for their project:
| ProjName | Explanation | Members | Tools |
| WebFlow | (FV for web flow algorithms) | Lalindra, Aravind, Amit | SPIN, others |
| KenKenSMT | Model games such as Kenken in SMT | Jared, Tyler, Matt | Z3 |
| Foci3DFV | FOCI 3D Verification | Sanjay, Ravindra, Raghav | Java Path Finder |
| PredAbs | Predicate Abstraction tool | Koushik, Thomas | Study PAM, BDD/SMT |
| AccessFV | Verifier for C | Balaji, Petey | Frama-C |
| Netbill | E-billing protocol | Sameeksha, Raghuveer | Promela |
| AirportSim | Simulate flows in an airport | Kay, Brad | Promela |
| SecureSW | Software Security | Dustin | CMU SEI tools |
| SMTProver | Gordon prover rewritten using SMT | Shuying | Yices, Z3 |
| CudaFV | FV methods for CUDA | Jinpeng | PUG, SMT tools |
| CacheFV | Cache protocol FV | Seth | Murphi |
| Cache2 | Compare Cache Protocol FV | Alireza | Murphi, NuSMV |
| Subtyping | Semantic Subtyping | Young Rok | SMT solvers, Dminor |
The final project presentations are to be made on April 26th. The presentation order is the same as with regular project 1-1 meeings. The project presentations will be held in our class room (LCR).
Your final project report must be formatted as per Springer LNCS guidelines. You may obtain Latex or Word files from the Springer site.
A significant percentage of your project grades will depend on how well written this paper is, and how much information/detail it reveals. It should also clearly document what each project member did (in a multi-person project). Please turn in the final project reports via handin to “project-reports.”
This course will cover several topics fundamental to computing, and illustrate them in realistic situations:
I will examine concrete situations to drive points home, with focus on formal specification, formal testing, and verification. Possible discussion topics include sequential software, concurrent software, pipelined execution units (CPUs, including multicore), GPU kernels, and CPU/GPU interactions, threaded programs, and communicating (message passing) processes.
This course will require you to program in Ocaml, as well as learn a fair amount of mathematical logic. It will also involve the use of several tools. Helpful references are attached:
~cs6110/bin, so please include that in your Unix path.Here are possible projects and tools involved:
A thorough understanding of Boolean algebra and basics of NFA, DFA, and Regular Expressions will be assumed. I hope to teach everything else through lectures and/or assigned readings (whose extent can vary depending on your background). If you don’t have a good computer science background, you will find functional programming and mathematical logic to be quite challenging. I am assuming enthusiasm to learn these topics, despite the hardships.
Grading will be based on class participation, assignments, and class projects. 10% is for class participation which includes regular attendance (please let me know if you have a reason to miss a lecture). 50% is for the class project. Class projects are to be done in groups of size 3 (smaller groups are allowed upon approval). Each group member must keep a record of their individual contributions.
I will be asking questions either to the class at large, or choose to ask questions to specific individuals, but in an encouraging way. I will make sure to remind you of previous material you have studied and lead you to the answer. I am sorry, this is the only way to make sure that you are participating in the class, and that is why I am announcing it during the first lecture itself.
40% is for assignments. Discussions are encouraged; however, unless otherwise indicated, your final submissions must be based on original effort. Please ask me if you think that you are exceeding the limits of “reasonable collaboration.”
There will also be many questions designed to be solved as a group. You are therefore encouraged to form your project groups early. Again, for each group solution, you should individually document your role.
Please read this link: http://www.eng.utah.edu/~cs6110/COE Guidelines Spring 2011.pdf.
This document was translated from LATEX by HEVEA.