Konstantine Arkoudas, developer of Athena, received the PhD in Computer Science from MIT (2000). His Master's thesis was declared an MIT MasterWork, at the bi-annual MIT event "honoring outstanding Master's theses in the EECS department." He graduated summa cum laude in 1993 with a BS in computer science from RPI, where he was the recipient of the annual Paul McGloin Prize, given to the "most outstanding" graduating senior in computer science. In dissertation work that puts him in perfect position for co-leading the MARMML team, Konstantine invented, defined, and implemented Athena, a new modern higher-order programming language incorporating a complete deduction system for polymorphic multi-sorted logic, and invented DPLs (denotational proof languages), a new approach to mechanized proofs. After obtaining his PhD from MIT, Arkoudas was a researcher in the MIT AI Lab, and authored a number of seminal technical reports during that time. Arkoudas left to work in industry as a Senior Engineer for DataSynapse Inc., where he worked on the security aspects of the DataSynapse distributed code platform. At DataSynapse he used the Java Cryptographic Extension to implement various encryption and decryption schemes, and implemented the Kerberos authentication protocol in Java. After industry he returned to MIT as a researcher in the Laboratory for Computer Science, and now, in connection with the MARMML project, has come to RPI as a research professor. His three most recent papers are:

• "Verifying a file system implementation"' co-authored with Karen Zee, Viktor Kuncak and Martin Rinard, to appear at the 2004 ICFEM (International Conference on Formal Engineering Methods), Seattle, USA, November 2004.
• "Deductive runtime certification" co-authored with Martin Rinard, 2004 Runtime Verification Methods conference, jointly with ETAPS 2004, April 2004, Barcelona, Spain.
• "Integrating model checking and theorem proving for relational reasoning," co-authored with Martin Rinard, Darko Marinov, and Sarfraz Khurshid, 7th International Seminar on Relational Methods in Computer Science (RelMiCS 7), Malente, Germany. May 2003.

Website
Curriculum Vitae

Projects:

DPLs
NDL

Publications