People

•  
•  
• Printable version

Faculty

• Patrice Chalin
• Ferhat Khendek
• Greg Butler

Collaborators, Partners and Related Projects

• Robby and John Hatcliff, SAnToS Laboratory:
  • JmlEclipse.
  • SparkAda (and SpAda).
  • Sireum/Kiasan for Java.
• Joe Kiniry (ITU), Mobius PVE.
• JML, LOOP, KeY.

Current Students

PhD

• George Karabotsos. Full Static Program Verification in the Verifying Compiler (tentative). Graduation: 2005-2011.

Masters

• Loren Segal. Program Verification (tentative). 2010-2012.

Graduates

PhD

• Stephen Barrett. Blending State Differences and Change Operations for Tool-Independent Merging of Software Models. Co-supervisor: Dr. Greg Butler. 2004-2011.
• Perry James. Enhancements to JML and its Extended Static Checking Technology. 2005-2009.
• Daniel Sinnig. Use Case and Task Models: Formal Unification and Integrated Development Methodology. Co-supervisor: Dr. F. Khendek, Concordia ECE. 2004-2008. Thesis accepted “as is”. Awarded the 2009-2010 ENCS Doctorial Prize.

Masters

• Stuart Thiel. Enterprise Application Design Patterns: Improved and Applied. 2005-2010.
• Asif Dogar. Model Driven Development for Enterprise Applications, 2006-2007 (fall).
• Rajiv Abraham. Model Driven Development: A Comprehensive Case Study, 2006-2007 (summer). Thesis accepted “as is”.
• Kianoush Torkzadeh. Requirements Specification of Business Transactions in Use Cases, 2006-2007 (spring).
• Hao Xi. Contributions to the JML Project: Safe Arithmetic and Non-null-by-default. M.Comp.Sc., 2004-2006 (fall).
• Frederic Rioux. Efficient and Effective Design by Contract for Java. M.Comp.Sc., 2004-2006 (spring).
• George Karabotsos. A Modern Isabelle-based Prover for VDM's Logic of Partial Functions. M.Comp.Sc., 2004-2005 (fall).
• Kui Dai. Enhancements to the JML Runtime Assertion Checker Compiler. M.Comp.Sc., 2003-2005 (fall).
• Louis-Julien Guillemette. MLPE: An Extensible Multi-Language Programming Environment. M.Comp.Sc., 2002-2004 (fall). Co-supervisor: Dr. Grogono.