Omkar Zade

I have recently completed my Master's degree in Computer Science at ETH Zürich, with major in Secure and Reliable Systems and minor in Machine Learning. I am now on the job market for positions in software engineering, security and machine learning.

I've taken courses and completed projects in network and system security, formal methods, high performance computing, probabilistic AI and so on. I also work part-time as a student assistant at Chair of Computational Social Sciences at ETH Zürich.

Before this, I completed my bachelor’s degree with the highest grade in computer science from VNIT Nagpur in 2018. After graduating, I worked as a Software Development Engineer at Amazon for 3 years on a variety of projects in the Fintech / Tax domain.

M.Sc. Computer Science. ETH Zürich.
Sep 2021 - April 2024. Major in Secure and Reliable Systems, Minor in Machine Learning.
Master thesis: Large Language Models for Verified Programs
Selected courses: System Security, Network Security, Design of Parallel and High Performance Computing, Probabilistic Artificial Intelligence, Computational Intelligence Lab, Formal Methods for Information Security, Principles of Distributed Computing, Machine Learning for Health Care

B.Tech. Computer Science & Engineering. VNIT, Nagpur, India.
2014-2018. CGPA 9.66/10 (Rank 1 of 99). Institute Medal
Excelled at foundational courses (including algorithms and data structures, discrete mathematics, computer networks, cryptography, operating systems, programming paradigms) and took many programming intensive courses. Took a variety of elective courses in AI, ML, Graph Theory, Image Processing, Bioinformatics etc.

Student Assistant. ETH Zürich.
Oct 2022 - Present. Chair of Computational Social Science.
Responsible for setting up and maintaining Apache servers, security analysis of the server and IoT devices, and software development in the area of traffic simulations and workflow orchestration.

Software Development Engineer II. Amazon, India.
2018 - 2021. Withholding Tax Platform.
-Revamped backend and frontend of TaxOpsManager - application used by Tax Operations at Amazon and its subsidiaries.
-Implemented appropriate authentication mechanisms to make the application accessible to clients external to Amazon
-Designed and implemented a scalable & configurable solution to launch the application in multiple tax jurisdictions, supporting Amazon’s rapid expansion.
-Responsible for mentoring and onboarding new team members, operational excellence, and technical hiring
Technologies: AWS StepFunctions, Lambda, API Gateway, CloudFormation, Cognito, DynamoDB, etc and internal CI/CD tools.

Large Language Models for Verified Programs
October 2023 - April 2024, ETH Zurich. Master thesis.
LLMs capable of generating code promise increased developer productivity, but we get no guarantees of correctness or safety from the generated programs. Program verification is a static analysis technique to prove that a program satisfies a formal specification - this gives much stronger guarantees than simply testing. However, these specifications and proofs need to be provided manually, and require expertise and time on part of the programmer. In this thesis, we leverage LLMs, in combination with feedback from an automatic verifier, to generate verified programs.
First, we evaluate prompt-engineering strategies on capable LLMs e.g. GPT-4. Next, we fine-tune open source LLMs (e.g. from Llama-2 family) on a dataset of verified programs that we have created. Finally, we investigate how such open source LLMs can be trained using reinforcement learning using verifier feedback as reward signal. We design a benchmark and perform extensive evaluation of our approaches.
Thesis: here | Code: here | Slides: here

Formal modeling and proofs of security protocol analyzer
Spring 2023, ETH Zurich. Semester Project.
Modeled and proved the correctness of a constraint-based security protocol analyzer in Isabelle/HOL. Formalized a unification algorithm for general first-order terms and showed its soundness, completeness, and termination. In the second part, specialized this theory to protocol messages and formalized constraint systems and a reduction relation, and showed it to be sound and terminating.

On the Computational Power of Neural Nets
ETH Zurich. Project for Advanced Formal Language Theory.
Analyzed and implemented the paper - "On the Computational Power of Neural Nets" (Siegelmann and Sontag, 1995). The paper is a famous result on the universality of first-order recursive nets, and has important consequences regarding decidability of such nets. Completed a constructive proof, by providing an implementation of the main theorem of the paper. In doing so, modeled the equations in the proof as efficient matrix- vector computations.
Report: here | Code: here

Tasking in DaCe
Fall 2022, ETH Zurich. Project for Design of Parallel & High Performance Computing.
DaCe is a fast parallel programming framework that takes code in Python/NumPy and other programming languages, and maps it to high-performance CPU, GPU, and FPGA programs. In this project, we modified DaCe to generate parallel code with OpenMP tasking and benchmarked its performance. Internally, DaCe uses the Stateful DataFlow multiGraph (SDFG) intermediate representation. We also implemented subgraph transformations to interactively map executions to parallel tasks.
Report: here

Collaborative Filtering
Spring 2022, ETH Zurich. Project for Computational Intelligence Lab.
Developed a novel approach to the recommender system problem (i.e. given a sparse user-movie rating matrix, fill in the missing entries) based on Matrix Factorization techniques such as SVD, Alternating Least Squares and Ensemble Learning. Our predictions surpassed the Netflix Prize baseline.
Report: here

Automatic Certificate Management Environment
Fall 2021, ETH Zurich. Project in Network Security.
Implemented the ACME protocol (specified in RFC 8555) and additional components (DNS Server, Challenge HTTP Server, ACME client) in Python. [Code is required to be private, but access can be granted on request]