Nikolaos Triantafyllou

Personal Information

PhD student at School of Electrical and Computer Engineering, NTUA
Graduated from School of Applied Mathematical and Physical Sciences, NTUA

Triantafyllou Nikolaos

Contact details

Research Interests

  • Formal methods
  • Specification and Verification
  • Algebraic Specification Languages
  • Code Generation
  • Automated theorem proving

Cafe2JML Project

The Cafe2JML project is a personal ongoing research project to generate executable code from behavioral (Observational Transition Systems mostly) algebraic specification code written in CafeOBJ (An algebraic specification language). The main idea of the project is to verify the behavior of a software system using the OTS/CafeOBJ method (that allows the verification of complex safety properties) and then obtain an implementation (in Java for now) which satisfies the specification.

Some first results can be found in this paper and this draft

The Cafe2JML is an opensource project and the code can be freely found at gitHub.This code can also be used as a parser for OTS/CafeOBJ specifications writen in Java. Within the next month the tool will be released and will be available freely.

Selected Publications

  • Nikolaos Triantafyllou, Petros S. Stefaneas, Panayiotis Frangos: An Algorithm for Allocating User Requests to Licenses in the OMA DRM System. IEICE Transactions 96- D (6):1258-1267 (2013)
  • Petros S. Stefaneas, Iakovos Ouranos, Nikolaos Triantafyllou, Katerina Ksystra: Some Engineering Applications of the OTS/CafeOBJ Method. Specification, Algebra, and Software 2014: 541-559
  • Nikolaos Triantafyllou, Iakovos Ouranos, Petros S. Stefaneas, Panayiotis Frangos: Formal Specification and Verification of the OMA License Choice Algorithm in the OTS/CafeOBJ Method. WINSYS 2010: 173-180
  • Nikolaos Triantafyllou, Katerina Ksystra, Petros S. Stefaneas, Panayiotis Frangos: Applying Algebraic Specifications on Digital Right Management Systems. ICCSW 2011: 94-100