Greg Dennis

email a@b where a=gdennis and b=alum.mit.edu

I am currently a Software Engineer at Google.

I was formerly a PhD student 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. At MIT, I developed techniques to check the conformance of object-oriented code to rich interface specifications. My prior research included the study of air-traffic control systems, the design of a radiation therapy machine, and contributions to the Alloy modeling language.


Projects:
Publications:
  • Emina Torlak, Mana Taghdiri, Greg Dennis, Joseph Near. Applications and Extensions of Alloy: Past, Present, and Future Mathematical Structures in Computer Science, Volume 23, August 2013, pp 915-933. Cambridge University Press. (PDF)
  • Derek Rayside, Aleksander Milicevic, Kuat Yessenov, Greg Dennis, and Daniel Jackson. Agile Specifications. OOPSLA Onward 2009. Orlando, Florida, October 2009. (PDF)
  • Greg Dennis. A Relational Framework for Bounded Program Verification. MIT PhD Thesis. July 2009. (PDF)
  • 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:
  • A Relational Framework for Bounded Program Verification. PhD Defense. June 2009. (PDF)
  • Bounded Verification of Voting Software. VSTTE '08. October 2008. (PDF)
  • Alloy Tutorial. HCSS '08. March 2008. (PDF)
  • Alloy Tutorial. FM '06. August 2006. (alloy.mit.edu/fm06)
  • Modular Verification of Code with SAT. ISSTA '06. July 2006. (PDF)
  • Automating Commutativity Analysis at the Design Level. ISSTA '04. July 2004. (PDF)

Other: