N. Ege Saraç

N. Ege Saraç

Approximately pronounced eh-GEH sah-RAHTCH

Marie Skłodowska-Curie Postdoctoral Fellow @ CISPA and TUM

N. Ege Saraç

About

I am a Marie Skłodowska-Curie Postdoctoral Fellow at the CISPA Helmholtz Center for Information Security and a visiting researcher at the Technical University of Munich (TUM), working in the Reactive Systems Group led by Bernd Finkbeiner. Before that, I completed my PhD in 2025 at the Institute of Science and Technology Austria (ISTA) under Tom Henzinger's supervision.

My research aims to help people build dependable computer systems. To this end, I develop theories and algorithms for formally specifying requirements and verifying systems against them.

A central motivation for my work is ensuring that these systems align with societal expectations such as privacy, fairness, and explainability. This is hard because these expectations often require reasoning about how multiple executions of a system relate to one another. Moreover, two systems may both satisfy the same requirements and still differ greatly in quality.

I work toward a unified framework for efficiently measuring how well systems satisfy such relational requirements, known as hyperproperties. In my MSCA Postdoctoral Fellowship project QHyperSTAR, I am laying the foundations for this framework by advancing the theory of quantitative hyperproperties and developing memory-efficient algorithms for monitoring them at runtime.

Selected Publications

Hyperproperties

  • TriCycle: Proving Temporal Hyperproperties, Coinductively

    POPL

    Arthur Correnson, N. Ege Saraç, Mishel Carelli, Bernd Finkbeiner

    We develop a coinductive proof system for temporal hyperproperties, enabling machine-checked proofs about relationships between infinite executions.

  • Quantitative Language Automata

    CONCUR pdf

    Thomas A. Henzinger, Pavol Kebis, Nicolas Mazzocchi, N. Ege Saraç

    We introduce the first dedicated specification language for quantitative hyperproperties, which assign values to sets or probability distributions of infinite executions.

Quantitative Verification

  • Extending QuAK with Nested Quantitative Automata

    CAV pdfcode

    Thomas A. Henzinger, Nicolas Mazzocchi, N. Ege Saraç, Harun Yılmaz

    We enable our tool Quantitative Automata Kit (QuAK) to automatically analyze performance measures whose values can grow arbitrarily large, such as response times.

  • Safety and Liveness of Quantitative Properties and Automata

    LMCS 21(2) pdf

    Udi Boker, Thomas A. Henzinger, Nicolas Mazzocchi, N. Ege Saraç

    We generalize the safety-liveness classification to quantitative properties and give decision procedures and decomposition algorithms for quantitative automata.

Runtime Monitoring

  • Quantitative and Approximate Monitoring

    LICS pdf

    Thomas A. Henzinger, N. Ege Saraç

    We develop a theory of quantitative runtime monitoring that formalizes how monitors estimate property values from finite observations.

  • Approximate Distributed Monitoring under Partial Synchrony: Balancing Speed and Accuracy

    RV pdfcode

    Borzoo Bonakdarpour, Anik Momtaz, Dejan Ničković, N. Ege Saraç

    We accelerate the monitoring of distributed systems with bounded clock skew using sound approximations that achieve speedups of up to five orders of magnitude.

News

Oct '26
Our paper TriCycle: Proving Temporal Hyperproperties, Coinductively is accepted for publication at POPL 2027.
Jun '26
Our paper Monitoring Discounted Sum Properties is accepted for publication at CONCUR 2026.
Apr '26
Our paper Extending QuAK with Nested Quantitative Automata is accepted for publication at CAV 2026.
Feb '26
My MSCA Postdoctoral Fellowship project Quantitative Hyperproperties: Specification, Taxonomy, and Runtime Monitoring (QHyperSTAR) has been selected for funding!
Feb '26
Our paper Quantitative Monitoring of Signal First-Order Logic is accepted for publication at FM 2026.