Greg Dennis


Greg Dennis
 Software Design Group
MIT Computer Science and Artificial Intelligence Laboratory
The Stata Center
32 Vassar Street, 32-G720
Cambridge, MA 02139
617-835-9161
email a@b where a=gdennis and b=mit.edu


I am a PhD student here at MIT in the Department of Electrical Engineering and Computer Science, and a member of the Software Design Group in the Computer Science and Artificial Intelligence Laboratory.

I am currently developing techniques to check the conformance of object-oriented code to rich interface specifications. As a member of SDG since my undergraduate years, my past research has included the study of air-traffic control systems, the design of a radiation therapy machine, and contributions to the Alloy modeling language.



Projects:

Publications:
  • Greg Dennis. A Relational Framework for Bounded Program Verification. MIT Ph.D. Thesis. June 2009.


  • Christopher Ackermann, Mikael Lindvall, Greg Dennis. Redesign for Flexibility and Maintainability: A Case Study. 13th European Conference on Software Maintenance and Reengineering (CSMR'09). Kaiserslautern, Germany, March 2009.


  • Greg Dennis, Kuat Yessenov, Daniel Jackson. Bounded Verification of Voting Software. Second IFIP Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE'08). Toronto, Canada, October 2008. (PDF)


  • Antonio Bucchiarone, Greg Dennis, and Stefania Gnesi. A Graph-based Design Framework for Global Computing Systems. Third International Workshop on Views On Designing Complex Architectures (VODCA'08). Bertinoro, Italy, August 2008.


  • Derek Rayside, Felix Chang, Greg Dennis, Robert Seater, and Daniel Jackson. Automatic Visualization of Relational Logic Models. First Workshop on the Layout of (Software) Engineering Diagrams (LED'07). Coeur d'Alene, Idaho, September 2007. (PDF)


  • Emina Torlak and Greg Dennis. Kodkod for Alloy Users. First Alloy Workshop, co-located with the 14th ACM/SIGSOFT Symposium on Foundations of Software Engineering (FSE'06). Portland, Oregon, November 2006. (PDF)


  • Greg Dennis, Felix Change, Daniel Jackson. Modular Verification of Code with SAT. International Symposium on Software Testing and Analysis (ISSTA'06). Portland, ME, July 2006. (PDF) (PS)


  • Greg Dennis, Robert Seater, Derek Rayside, Daniel Jackson. Automating Commutativity Analysis at the Design Level. International Symposium on Software Testing and Analysis (ISSTA'04). Boston, MA, July 2004. (PDF) (PS)


  • Greg Dennis. TSAFE: Building a Trusted Computing Base for Air Traffic Control Software. MIT Masters Thesis, January 2003. (PDF) (PS)



Talks:
  • Automating Commutativity Analysis at the Design Level (PDF)



Other: