Formal Methods Projects

Problems

If you have an idea for a project involving formal methods or want to ask me about other possible projects, come by my office or send email. Some possible topics, many of which can lead to publishable results, include the following.

• Safety and liveness in branching time logics. There are many theoretic and practical issues.
• Applying formal methods to compiler verification.
• Towards a library of theorems for reasoning about the ordinals in ACL2.
• A survey of the theory and implementation of lazy evaluation.
• Notions of correctness for reactive systems.
• A survey of data independence, a technique for reducing infinite-state systems to finite state systems that has been used to verify communications protocols and cryptographic protocols.
• Algorithms for out-of-core model checking.
• Out-of-core BDDs.
• A survey of techniques for combining model checking and theorem proving.
• Extraction of symbolic quotient structures from well-founded bisimulation proofs.

The evaluation will be based on a short report of your findings. If the report is well written and it is clear that the project was given serious consideration, I will assign an A. One way that I can determine that the project was considered seriously is if you talk to me.