Term Projects for CSI 5110 (COMP 5707)

Project Topics

• Your term project can take one of the following 2 forms. (If you prefer a different kind of project, please speak with your professor.)

1. A program that implements a theorem prover or model checker of some kind. Examples include:
   • A program for building natural deduction proofs for propositional logic. At each step the program asks what inference rule the user wants to apply. The program keeps some representation of the proof as it proceeds, and prints it out in a readable format at the end. You might also try to determine which rules are applicable and output a list of possible rules to apply that the user can choose from. If there is only one rule to apply, you could apply it without asking the user, but instead, just informing him/her.
   • A program for building proof tableaux for program verification. Similar to above, but with the proof calculus from Chapter 4. In this case, you can apply most of the rules automatically. The user will only have to help with the application of the "while" rule.
   • An automated theorem prover for propositional or first-order logic using a strategy of your choice.
2. A paper on at least 2 research articles in the areas of theorem proving and/or model checking. The papers must be closely related enough to compare the approaches taken in each. For example, you might compare two formal verifications of similar programs/protocols, and compare the use of the two systems in which the verifications were done. Places to find papers include:
   • Proceedings of the Conference on Automated Deduction or the International Conference on Theorem Proving in Higher Order Logics. Both of these proceedings are part of the Springer-Verlag Lecture Notes in Computer Science Series and are available at Morisset Library.
   • Journal of Automated Reasoning (Many issues can be found in my office.)
   • Example Project: Compare different approaches to proof-carrying code, or compare proof-carrying code to related techniques for certifying the safety of software. For example, see:
     • George Necula's proof-carrying code page,
     • Peter Lee's proof-carrying code page,
     • proof-carrying code at Princeton's Secure Internet Programming Lab
     • Mobile Resource Guarantees project
     • The Mobius research project
     • the FLINT project and, in particular, Zhong Shao's publications
     • the ConCert project and, in particular, Karl Crary's publications
     • typed assembly language
     • a paper on decentralized trust management
     • a paper on software fault isolation
     • the PittSFIeld software fault isolation project
   • Another Example Project: Compare two or more applications of formal methods in practice. At least one of the case studies must use a logic-based method such as theorem proving or model checking. The books listed below are one place to start looking. They will be put on reserve for this course in the library so that they can be borrowed for 48 hours at a time. Note that in the first, all case studies use the ACL2 theorem prover, and in the other two, very few of the case studies use logic-based formal methods. Also, I have copies of the last two, which you can borrow from me for a few days at a time.
     • Computer-aided reasoning: ACL2 case studies, Matt Kaufmann, Panagiotis Manolios, J. Strother Moore, eds. Kluwer Academic Publishers, 2000.
     • Industrial-strength formal methods in practice, Michael G. Hinchey and Jonathan P. Bowen, eds. Springer, 1999.
     • Applications of formal methods, Michael G. Hinchey and Jonathan P. Bowen, eds. Prentice Hall, 1995.
   • The links below are to projects, methods, and tools and they include links to papers published on results of these projects and related areas.
     • The Coq Proof Assistant
     • The PVS Specification and Verification System
     • Isabelle Generic Proof Assistant
     • The Java Modelling Language (JML)
     • The Krakatoa Tool for Java Program Verification
     • The KeY Project: Integrated Deductive Software Design
     • ACL2: A semi-automatic theorem prover for modelling and reasoning about computer systems
     • Prover9: An Automated Theorem Prover for First-Order and Equational Logic
     • The Twelf system for specifying, implementing, and proving properties of programming languages and logics
     • The Alloy Analyzer
     • Spin model checker
     • NuSMV: a symbolic model checker
     • Murphi Model Checking Verifier Tool
     • Database of Rewriting Systems
     • The World Wide Web Virual Library: Formal Methods

Project Evaluation

• You will be expected to give a 10-15 minute presentation on your project or paper on November 27. Click here for tips on how to give a good short presentation. (Note: These tips were prepared for CSI 4900 and not all of it applies to CSI 5110. For example, the part about demos does not apply.)
• The presentation schedule is as follows:
  • Thursday, November 27, 10:00-11:30
    • Dishant Langayan
    • Michel St-Martin
    • Dianshu Hu
• A report on your project is due on November 27. The contents of the report depend on which project option you have chosen, as listed below. Please consult guidelines regarding plagiarism.
  1. For programs implementing a theorem prover or model checker, the report should include:
     • A short paper (approximately 5 pages or so) which explains and documents your program, so that a user may both run it and understand the structure of the code. It is also important to include analysis in your report, i.e., information about things such as design decisions that came up along the way, the reasons you decided to take a particular approach, etc. You must hand in a hard copy of this paper.
     • Your code in an electronic format so that it can be executed. You must make an appointment with me to install your software on my computer on either Windows XP or Linux. It is your responsiblity to make sure it runs. The installation must include your source code.
  2. For papers on research articles, there is no strict number of pages required for your paper, but you will probably need around 20 pages to explain the material and include your own comparison and analysis. You must hand in a hard copy of your paper.