Verifying Security Protocols for Sensor Networks Using Algebraic Specification Techniques. - Iakovos Ouranos; Petros S. Stefaneas (CAI, 2007)

A Formal Specification Framework for Ad Hoc Mobile Communication Networks. - Iakovos Ouranos; Petros S. Stefaneas; Panagiotis Frangos (SOFSEM (2), 2007)

An Algebraic Framework for Modeling of Mobile Systems. - Iakovos Ouranos; Petros S. Stefaneas; Panagiotis Frangos (IEICE Trans. Fundam. Electron. Commun. Comput. Sci., 2007)

Algebraic Specifications for OMA REL Licenses. - Nikolaos Triantafyllou; Iakovos Ouranos; Petros S. Stefaneas (WiMob, 2009)

Using the OTS/CafeOBJ Method to Formally Specify and Verify the Open Mobile Alliance License Choice Algorithm. - Nikolaos Triantafyllou; Iakovos Ouranos; Petros S. Stefaneas; Panayiotis Frangos (ICETE (Selected Papers), 2010)

Formal Modeling and Verification of Sensor Network Encryption Protocol in the OTS/CafeOBJ Method. - Iakovos Ouranos; Petros S. Stefaneas; Kazuhiro Ogata 001 (ISoLA (1), 2010)

A Parallel Version of the MPEG-2 Encoding Algorithm Formally Analyzed using Algebraic Specifications. - Katerina Ksystra; Petros S. Stefaneas; Iakovos Ouranos; Panayiotis Frangos (SIGMAP, 2010)

Formal Specification and Verification of the OMA License Choice Algorithm in the OTS/CafeOBJ Method. - Nikolaos Triantafyllou; Iakovos Ouranos; Petros S. Stefaneas; Panayiotis Frangos (WINSYS, 2010)

Towards a correct translation from ASN.1 into CafeOBJ. - Konstantinos Barlas; George Koletsos; Petros S. Stefaneas; Iakovos Ouranos (Int. J. Reason. based Intell. Syst., 2010)

Redesigning the Open Mobile Alliance License Choice Algorithm - Nikolaos Triantafyllou; Petros S. Stefaneas; Iakovos Ouranos; Panayiotis Frangos; Katerina Ksystra (CoRR, 2011)

Formal Analysis of TESLA Protocol in the Timed OTS/CafeOBJ Method. - Iakovos Ouranos; Kazuhiro Ogata 001; Petros S. Stefaneas (ISoLA (2), 2012)

Towards a Protocol Algebra Based on Algebraic Specifications. - Iakovos Ouranos; Petros S. Stefaneas (SERA (selected papers), 2013)

Some Engineering Applications of the OTS/CafeOBJ Method. - Petros S. Stefaneas; Iakovos Ouranos; Nikolaos Triantafyllou; Katerina Ksystra (Specification, Algebra, and Software, 2014)

TESLA Source Authentication Protocol Verification Experiment in the Timed OTS/CafeOBJ Method: Experiences and Lessons Learned. - Iakovos Ouranos; Kazuhiro Ogata 001; Petros S. Stefaneas (IEICE Trans. Inf. Syst., 2014)

Formalizing Air Traffic Control Regulations in PSOA RuleML. - Theodoros Mitsikas; Sofia Almpani; Petros S. Stefaneas; Panayiotis Frangos; Iakovos Ouranos (RuleML+RR (Supplement), 2018)

Aligning, Interoperating, and Co-executing Air Traffic Control Rules Across PSOA RuleML and IDP. - Marjolein Deryck; Theodoros Mitsikas; Sofia Almpani; Petros S. Stefaneas; Panayiotis Frangos; Iakovos Ouranos; Harold Boley; Joost Vennekens (RuleML+RR, 2019)