Atalay Mert Ileri

Atalay Mert Ileri

he/him

Postdoctoral researcher at University of Oxford working on formal verification, type systems, and quantum processes.

Publications

You can also find my articles on my Google Scholar profile.

Conference Papers

VEL: A Formally Verified Reasoner for EL++ Description Logic.

Published in ISWC 2024 Poster Track, 2024

Over the past two decades, the Web Ontology Language (OWL) has been instrumental in advancing the development of ontologies and knowledge graphs, providing a structured framework that enhances the semantic integration of data. However, the reliability of deductive reasoning within these systems remains challenging, as evidenced by inconsistencies among popular reasoners in competitions. This evidence underscores the limitations of current testing-based methodologies, particularly in high-stakes domains such as healthcare. To mitigate these issues, in this study, we have developed VEL, a formally verified ℰℒ++ reasoner equipped with machine-checkable correctness proofs that ensure the validity of outputs across all possible inputs. This formalization, based on the algorithm of Baader et al.[1], has been transformed into executable OCaml code using the Coq proof assistant’s extraction capabilities. In addition to producing a correct implementation, our work uncovered two errors in the published completeness proof that required a modification to the original algorithm.

Download Paper

Probability from Possibility: Probabilistic Confidentiality for Storage Systems Under Nondeterminism

Published in CSF 2024, 2024

Nondeterminism, such as system crashes, poses an important challenge to the security of storage systems by making leakages possible through secret-dependent result probabilities. This paper proposes a new possibilistic confidentiality specification prohibiting such probabilistic leakages. Our specification is preserved under simulation to enable modularity and is sequentially compositional. We implemented our specification in a framework that contains structures to implement storage systems and prove their confidentiality in a modular fashion. On top of our framework, we implemented the first crash-safe file system with a termination-insensitive version of our specification and machine-checkable confidentiality proofs. Our evaluation shows that proving confidentiality incurs 9.2x proof overhead per line of implementation code. Both our framework and file system are implemented in Coq and extracted to Haskell to obtain an executable artifact.

Download Paper