Naso Evangelou-Oost

General Purpose South 78-414

The University of Queensland

St Lucia, Qld 4067

I’m Naso Evangelou-Oost, a third-year PhD Candidate at the University of Queensland, School of Electrical Engineering and Computer Science (EECS). My academic journey is deeply rooted in a fascination with mathematics and computer science, leading me to explore intricate realms like valuation algebras and sheaf theory.

PhD Candidate - The University of Queensland, EECS

In the world of concurrent and distributed systems, complexity abounds. Through my PhD research, I’ve sought to illuminate this complexity by applying valuation algebras and sheaf theory to formal methods. My work is driven not only by intellectual curiosity but by a genuine desire to enhance the efficiency and reliability of the digital infrastructure that connects our world.

Research Interests:

Valuation Algebras: A foundation that allows me to explore abstract algebraic structures with a broad range of applications.
Sheaf Theory: A powerful tool for understanding local behaviours in mathematical contexts, a concept that greatly enriches my studies.
Formal Methods: Investigating precise ways of specifying and verifying complex software systems to ensure their correct operation.
Concurrent and Distributed Systems: Striving to make the technology that underpins modern life more robust and resilient.

Founder - Oneironaut

Beyond academia, I’m the founder of Oneironaut, a mathematical software consultancy. Here, I combine my passions for category theory, artificial intelligence, machine learning, and functional programming to create tailor-made solutions to complex problems. It’s not about using the latest buzzwords or tech trends; it’s about applying deep mathematical insight to real-world challenges in knowledge representation & reasoning and predictive analytics.

Oneironaut is an embodiment of my commitment to innovative thinking, enabling me to craft bespoke solutions that are both effective and novel. My work serves as a bridge between abstract theory and practical application, and I continually strive to translate mathematical concepts into tangible value for my clients.

Selected publications

Trace Models of Concurrent Valuation Algebras

Naso Evangelou-Oost, Larissa Meinicke, Callum Bannister, and 1 more author

In Formal Methods and Software Engineering, 2023

Abs Bib

This paper introduces Concurrent Valuation Algebras (CVAs), a novel extension of ordered valuation algebras (OVAs). CVAs include two combine operators representing parallel and sequential products, adhering to a weak exchange law. This development offers theoretical and practical benefits for the specification and modelling of concurrent and distributed systems. As a presheaf on a space of domains, CVAs enable localised specifications, supporting modularity, compositionality, and the ability to represent large and complex systems. Furthermore, CVAs align with lattice-based refinement reasoning and are compatible with established methodologies such as Hoare and Rely-Guarantee logics. The flexibility of CVAs is explored through three trace models, illustrating distinct paradigms of concurrent/distributed computing, interrelated by morphisms. The paper also highlights the potential to incorporate a powerful local computation framework from valuation algebras for model checking in concurrent and distributed systems. The foundational results presented have been verified with the proof assistant Isabelle/HOL.
@inproceedings{evangelouoost2023a, address = {Singapore}, author = {Evangelou-Oost, Naso and Meinicke, Larissa and Bannister, Callum and Hayes, Ian J.}, booktitle = {Formal Methods and Software Engineering}, editor = {Li, Yi and Tahar, Sofi{\`e}ne}, isbn = {978-981-99-7584-6}, pages = {118--136}, publisher = {Springer Nature Singapore}, title = {Trace Models of Concurrent Valuation Algebras}, year = {2023} }
Contextuality in Distributed Systems

Nasos Evangelou-Oost, Callum Bannister, and Ian J. Hayes

In Relational and Algebraic Methods in Computer Science, 2023

Abs Bib

We present a lattice of distributed program specifications, whose ordering represents implementability/refinement. Specifications are modelled by families of subsets of relative execution traces, which encode the local orderings of state transitions, rather than their absolute timing according to a global clock. This is to overcome fundamental physical difficulties with synchronisation. The lattice of specifications is assembled and analysed with several established mathematical tools. Sets of nondegenerate cells of a simplicial set are used to model relative traces, presheaves model the parametrisation of these traces by a topological space of variables, and information algebras reveal novel constraints on program correctness. The latter aspect brings the enterprise of program specification under the widening umbrella of contextual semantics introduced by Abramsky et al. In this model of program specifications, contextuality manifests as a failure of a consistency criterion comparable to Lamport’s definition of sequential consistency. The theory of information algebras also suggests efficient local computation algorithms for the verification of this criterion. The novel constructions in this paper have been verified in the proof assistant Isabelle/HOL.
@inproceedings{evangelouoost2023b, address = {Cham}, author = {Evangelou-Oost, Nasos and Bannister, Callum and Hayes, Ian J.}, booktitle = {Relational and Algebraic Methods in Computer Science}, editor = {Gl{\"u}ck, Roland and Santocanale, Luigi and Winter, Michael}, isbn = {978-3-031-28083-2}, order = {4}, pages = {52--68}, publisher = {Springer International Publishing}, title = {Contextuality in Distributed Systems}, url = {https://link.springer.com/chapter/10.1007/978-3-031-28083-2_4}, year = {2023} }