To gain the knowledge and skills necessary to confidently perform credible research in the V&V lab.
Estes is named after Richard Estes who is a photo-realistic painter. Estes is named Estes because it is an approach to model checking that attempts to use an extremely realistic formal model. Similarly, photo-realistic art is extremely realistic.
Your Advisor and your Senior RA will work with you to complete the immersion process.
1. Create your own blog. See http://vv.cs.byu.edu/blog/ for instructions on how to create your blog. Once you’ve created your blog, send the URL to your advisor and Senior RA. They’ll follow your progress in your blog entries.
2. Superficially read the immersion papers (listed below). “Superficially read” means read mostly just the abstract, introduction and conclusion to get the main idea of the paper—even if you don’t completely understand it. Pick 3 papers that your find most interesting to study in depth. You should pick at least one paper from each group of papers. For each of the three papers, create an entry in your blog that answers question 6 of the literature search pattern for each paper. Remember that the paper’s author could conceivably read your entry. So be accurate and be diplomatic.
3. Learn how to use CVS. Be comfortable checking out modules, committing changes, and resolving conflicts.
4. Write a program for an embedded processor supported by Estes. Write an Estes environment to provide input to your program. Identify and prove a correctness property. Add your program to the software-mc repository. Document an error in your program that can be easily removed and added as necessary. Collect the number of states, size of the state vector, average branching factor and number of errors. Add a file with these metrics to the emc_benchmarks/estes directory.
5. Read the code base documentation collection (various README files in software-mc).
6. With your advisor and Senior RA, identify something to extend or improve in the Estes code base. Complete the modification. Write about your experience modifying the code base. This document will be used by future new lab members.
7. Identify ways to improve the immersion process.
After completing the immersion process, you will be qualified to work with a Senior RA with the goal of co-authoring a publishable paper. After co-authoring your first paper, you will become a Senior RA and begin working with Junior RAs.
Not catching the big picture of the lab. A symptom of this is that you can not explain your research and why its important to your parents or roommates.
This group of papers focuses on software veficiation using explicit model checking.
1.
Chapters 1 and 9 of Model Checking by Clarke, Grumberg and
Peled (available in the lab).
2.
Addressing
Dynamic Issues in Program Model Checking, F. Lerda and W. Visser, SPIN 2001:
describes the structure and implement of Java Path Finder (JPF) including
collapsed states, sibling caching, and child lookahead. These are important ideas in the
implementation of Estes.
3.
Data
flow analysis is model checking of abstract interpretations, D.
Schmidt. SIGPLAN 1998. The theory can be a little daunting
in this paper, but the main message is very valuable.
4.
Software
Model Checking: The VeriSoft Approach, P. Godefroid. Lucent
Technologies August 1, 2003.
5.
Model
Checking Programs , Willem
Visser et al. Automated Software
Engineering Journal, V. 10, N. 2, April 2003.
6.
Model Driven
Software Verifiation, G. Holzmann and R. Joshi in SPIN 2004. An interesting description of a data
abstraction idea.
7.
Bebop:
A Symbolic Model Checker for Boolean Programs, T. Ball and S. Rajamani in
SPIN 2000.
This group of papers deals with capacity problems in general
purpose explicit model checking.
1.
Parallelizing
the Murphi Verifier, Ulrich Stern and David L. Dill, 9th International
Conference on Computer Aided Verification, 1997
2.
Using
Magnetic Disk instead of Main Memory in the Murphi Verifier, Ulrich Stern
and David L. Dill, CAV '98.
3.
Exploiting
Transition Locality in the Disk Based Murphi Verifier, Giuseppe Della
Penna, Benedetto Intrigila, Enrico Tronci, Marisa Venturini Zilli, Formal
Methods in Computer-Aided Design (FMCAD) , 6-8/11/2002.
4.
Directed
Explicit Model Checking with HSF-SPINStefan Edelkamp, Alberto Lluch
Lafuente, and Stefan Leue, SPIN 2001.
5.
Computational
Experiments with Parallel Algorithms: Issues, Measures, and Experts' Opinions,
Richard S. Barr and Betty S. Hickmann, ORSA Journal on Computing Volume 5, No.
1, 1993 The "Tar
Baby" of Computing: Performance Analysis, John L. Gustafson, ORSA
Journal on Computing Volume 5, No. 1, 1993
6.
A
Work-efficient Distributed Algorithm for Reachability Analysis, Orna
Grumbert, Tamir Haymen, and Assaf Schuster, CAV, July, 2003