Ferhat Erata

Ferhat Erata

PhD Candidate at Yale | Applied Scientist Intern at Amazon AI

Yale University

Amazon AI

Biography

I am pursuing a PhD in Computer Science at Yale University under the guidance of Ruzica Piskac and Jakub Szefer. My current research focuses on the automated inference of program properties and invariants by integrating machine learning with formal methods.

Currently, I am an Applied Scientist Intern at the Automated Reasoning Group in AWS, working on neurosymbolic programming to capture symbolic knowledge and mitigate hallucinations of LLMs in logical reasoning. Previously, I developed tools for model-based conformance checking of distributed networked systems at AWS.

During my PhD, I focused on verifying the side-channel insecurity of low-level Post-Quantum Cryptographic code (EuroS&P 2023). My work included reverse engineering quantum circuits from power traces (CHES 2024, CCS 2023), exploring quantum fault injections (QCE 2024), and detecting quantum computer viruses (HOST 2023). Additionally, I developed a tool for analyzing the non-functional behaviors of intermittent programs (TECS 2023), developed a software countermeasure against physical attacks (ICCAD 2024), and surveyed security verification techniques (JETC 2023). Before my PhD, I worked as a research software engineer in industry, applying formal methods to engineering problems (COMPSAC 2019, FSE 2018, FSE 2017, ASE 2017, SAC 2017).

Interests
  • Automated Reasoning
  • Program Synthesis
  • AI/ML for Code
  • Neurosymbolic Computing
  • System Security
  • Software Engineering
Education
  • PhD in Computer Science, 2025

    Yale University, CT, US

  • MSc, MPhil in Computer Science

    Yale University, CT, US

  • MSc in Information Technologies

    Ege University, Izmir, TR

  • BSc in Computer Science

    Dokuz Eylul University, Izmir, TR

Experience

 
 
 
 
 
Yale University
Graduate Research Assistant & Teaching Fellow
June 2020 – Present New Haven, CT, US

Research Asistant:

Teaching Asistant:

 
 
 
 
 
Amazon AI
Applied Scientist Intern
May 2024 – Present New York, NY, US
Automated Reasoning Group (ARG) – Working on Neurosymbolic Program Synthesis to capture symbolic knowledge and detect hallucinations of LLMs in logical reasoning.
 
 
 
 
 
Amazon Web Services (AWS)
Applied Scientist Intern
May 2023 – January 2024 New York, NY, US
Automated Reasoning Group (ARG) – Developed a scheduler framework for randomized testing, model-based testing, and conformance checking of distributed AWS Services in Rust.
 
 
 
 
 
Amazon Web Services (AWS)
Applied Scientist Intern
June 2022 – January 2023 New York, NY, US
Automated Reasoning Group (ARG) – Developed a decision procedure in Rust programming languages for checking linearizability of distributed systems.
 
 
 
 
 
ITEA4 Project: XIVT--eXcellence In Variant Testing
National Consortium Leader, Software Research Engineer
October 2018 – August 2019 Ege University, Izmir, TR
I developed AlloyInEcore for Automated Model Reasoning from Alloy Specifications. Published in FSE 2018 and contributed to a Model-based Testing framework IEEE Access.
 
 
 
 
 
ITEA3 Project: ASSUME--Safe & Secure Mobility Evolution
National Consortium Leader, Software Research Engineer
September 2015 – December 2018 Ege University, Izmir, TR
I developed Tarski Automated Reasoning tool for Traces based on Formal Semantics. Published in FSE 2017 and SAC 2017.
 
 
 
 
 
ITEA2 Project: Text & Model-Synchronized Document Engineering
Project Leader, Software Research Engineer
January 2014 – September 2017 Ege University, Izmir, TR
I led the development of ModelWriter–Text and model-synchronization engineering platform. Published in ASE 2017.

Service

 
 
 
 
 
European Cooperation in Science and Technology (COST)
Management Committee Member
December 2017 – January 2019
 
 
 
 
 
European Cooperation in Science and Technology (COST)
Management Committee Member
January 2015 – January 2019

Publications

See all publications by filtering.
(2024). Quantum Circuit Reconstruction from Power Side-Channel Attacks on Quantum Computer Controllers. IACR Transactions on Cryptographic Hardware and Embedded Systems (TCHES).

PDF Cite Project Slides Video DOI URL

(2024). Systematic Use of Random Self-Reducibility in Cryptographic Code against Physical Attacks. IEEE/ACM International Conference on Computer-Aided Design (ICCAD).

PDF Cite Project Slides Video DOI

(2024). Classification of Quantum Computer Fault Injection Attacks. IEEE International Conference on Quantum Computing and Engineering (QCE).

PDF Cite Project DOI URL

(2023). Exploration of Power Side-Channel Vulnerabilities in Quantum Computer Controllers. ACM SIGSAC Conference on Computer and Communications Security (CCS).

PDF Cite Project DOI URL

(2023). Towards Automated Detection of Single-Trace Side-Channel Vulnerabilities in Constant-Time Cryptographic Code. European Symposium on Security and Privacy (EuroS&P).

PDF Cite Slides Video DOI URL

(2023). ETAP: Energy-aware timing analysis of intermittent programs. ACM Transactions on Embedded Computing Systems (TECS).

PDF Cite DOI URL

(2023). Survey of approaches and techniques for security verification of computer systems. ACM Journal on Emerging Technologies in Computing Systems (JETC).

PDF Cite DOI URL

(2023). AdapTV: A Model-Based Test Adaptation Approach for End-to-End User Interface Testing of Smart TVs. IEEE Access.

PDF Cite DOI URL

(2023). Design of Quantum Computer Antivirus. International Symposium on Hardware Oriented Security and Trust (HOST).

PDF Cite DOI URL

(2020). A survey on the practical use of UML for different software architecture viewpoints. Information and Software Technology.

PDF Cite DOI URL

(2020). Automated reasoning framework for traceability management of system of systems. Science of Computer Programming.

PDF Cite DOI URL

(2019). Integrating static code analysis toolchains. IEEE 43rd Annual Computer Software and Applications Conference (COMPSAC).

PDF Cite DOI URL

(2018). AlloyInEcore: embedding of first-order relational logic into meta-object facility for automated model reasoning. Proceedings of Foundations of Software Engineering (ESEC/FSE).

PDF Cite DOI URL

(2017). A tool for automated reasoning about traces based on configurable formal semantics. Proceedings of Foundations of Software Engineering (ESEC/FSE).

PDF Cite DOI URL

(2017). ModelWriter: Text and model-synchronized document engineering platform. 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE).

PDF Cite DOI URL

(2017). Tarski: A platform for automated analysis of dynamically configurable traceability semantics. Symposium on Applied Computing (SAC).

Cite DOI URL

Featured Projects

Contact