CISC835: Formal Methods in Software Engineering (Fall 2019) Projects

Choosing a project

• Apply the course material to a new problem; e.g., use one or more of the languages and tools presented in the course to formalize and analyze one or more problems or puzzles (e.g., the RushHour puzzle www.puzzles.com/products/rushhour/rhfrommarkriedel/Jam.html). You might even be able to find a suitable problem in your area of research.
• Explore work that extends the material discussed in class; e.g., you could investigate and experiment with any of the tools mentioned below in the list of tools or compare some of them with tools discussed in class or other tools on the list.

Proposal

Presentation

Please note:

• Each presentation has a 25 mins slot. Of these 25 mins, 20 mins should be used for the presentation itself, while the remaining 5 mins are for questions and discussion. Please ensure that your presentation does not take longer than 20 mins. If you do take longer, I will have to interrupt you.
• The 5 mins discussion period will also be used to allow the next speaker to get ready.
• Please make sure prior to your presentation that your laptop works with the data projector in the class room.
• The content of each presentation should
  • be understandable to the majority of the members in the class,
  • explain any background or context information or material necessary to understand or appreciate what you have done,
  • summarize what you have done and why it is interesting and worth doing,
  • briefly describe how you have done it,
  • mention which results you have obtained and what you have learned (e.g., what would you do differently next time?),
  • share any additional observations that you feel are relevant or interesting.
• The presentation slides should
  • be correct, clear, readable and easy to navigate; typically, that means that slides should not contain a lot of text; highlighting of text can be very useful to emphasize key points; diagrams can be very useful to communicate concepts and relationships effectively, and
  • support and be connected to what you say.
• The delivery of the presentation should be clear, engaging and easy-to-follow, i.e., try to speak clearly with appropriate pace (i.e., neither too fast, nor too slow) and good eye contact.

Final report

Evaluation

• Presentation: 7%
• Proposal and final report: 6%
• Evaluation (i.e., overall difficulity and quality of work carried out): 7%

Project presentation schedule

1. 1:30-2pm, "Exploration of different versions of Alloy" (Sahil)
2. 2-2:30pm, "Using Alloy Analyzer to Model a Solution to the Assignments Problem Through the Context of Post-Secondary Roommate Matching" (Robyn)
3. 2:30-3pm, "Survey of Formal Verification Techniques for Deep Neural Networks" (Rebecca)
4. 3-3:30pm, "Monitoring Events using the BeepBeep 3 Event Stream Processor" (Isra and Mufasir)
5. 3:30-4pm, "Higher-Order Model Checking, Program Verification, and Refinement Typing" (Dimitrios)

Tools list

1. Propositional and predicate logic
   • A list of theorem proving tools can be found here.
   • Constraint solving generalizes checking for satisfiability or validity discussed in class; constraint solving is discussed in more detail here. Popular constraint solvers include: Z3 from Microsoft and Choco.
2. Class modeling
   • A list of applications of Alloy can be found here.
   • DynAlloy is an extension of Alloy that allows the description of dynamic (i.e., behavioural) properties using actions.
   • Alloy* is an extension of Alloy that expands the set of specification that can be analyzed (by supporting quantification over higher-order structures such as relations)
   • A list of other tools built on Alloy (or its underlying model finding technology) can be found here.
   • The Object Constraint Language (OCL) is a more mainstream technique to express object constraints. You can find a description of OCL here. Popular OCL tools include USE and and Dresden OCL. A more complete list of OCL tools is here.
   • The Java Modeling Language (JML) allows the embedding of formal specifications and constraints right in Java. Supporting tools are listed on the JML pages.
3. Model checking
   • Apart from NuSMV, Spin is one of the most well-known model checkers.
   • Java Pathfinder is a software model checker, i.e., it can explore the state spaces of Java programs directly and without prior translation to some tool-specific input language.
   • For finite state machines with time (a.k.a., Timed Automata), the UppAal is most widely used
   • For finite state machines with probabilities on the transitions (a.k.a, Markov Chains), the PRISM model checker is the state-of-the-art.
4. Other verification and analysis tools
   • The Rise 4 Fun site contains lots of tools for different kinds of analyses.
5. Formal methods for deep learning
   • Neural nets have proven very useful. However, to be able to use them in safety critical applications, we need to be able to validate, verify, and even certify them. Research on this topic is still in its infancy. The project could survey some of the ideas that have been proposed.
6. Machine learning for formal methods
   • Could machine learning be leveraged for the formal analysis of software artifacts? Could, e.g., learning techniques be used to learn formal specifications, find useful abstractions for complex systems, or fine tune and optimize the use of an analysis tool? The project could survey some of the ideas that have been proposed.

Last modified: Wed Nov 30 17:17:06 EST 2016