about ME

Ph.D. candidate at the Computer Science Department, Technion, Israel

Father of two extraordinary beings and husband to the one who always knows best.
Master of my domain (when I'm home alone). 
I really love to build. Whether it's a program, a website, a video game for my daughter, or even a bench for the lobby, each creation is a new source of joy. I also enjoy working on hard computational and mathemaical problems, and to find an elegant solution. 

Contact Information

 

Papers

Easter Egg: Equality Reasoning Based on E-Graphs with Multiple Assumptions

Many recent works use Equality Graphs (E-graphs) as the basis for their deductive reasoning. E-graphs are very useful for their compactness, congruence closure property, and lately, for running equality saturation. While e-graphs are effective, when it comes to conditional reasoning, such as case splitting, they are quite limited. The problem comes from their constructive nature, once a deduction is made, it cannot be easily removed. Usual solutions include copying the entire e-graph or parts of it. In this work we introduce Colored E-Graphs, implemented on top of the egg library. Colored e-graphs efficiently represent multiple copies of an e-graph, thus enabling efficient conditional reasoning during equality saturation. By carefully optimizing the new set of e-graphs, colroed e-graphs reach 10X memory usage reduction, and a small runtime improvement.

code

Condition synthesis realizability via constrained horn clauses

Program repair aims to automatically fix bugs, improving software reliability by handling issues that are often difficult to diagnose. One tricky aspect is dealing with missing or faulty conditions, which can lead to persistent, elusive errors. COSYN tackles this challenge by identifying "doomed initial states"—situations where, no matter how you patch the conditions, an error is inevitable. These states, in combination with reducing the problem to Constrained Horn Clauses and applying a CHC solver, allows COSYN efficiently determines whether a fix is possible. This method not only outperforms tools like CVC5, especially in proving unrealizability, but also provides a clearer path to synthesizing the correct conditions when a repair is viable.

code

Theory Exploration Powered By Deductive Synthesis

It is common for formal methods to receive a set of lemmas as input. It could be for compiler optimization, program verification, or program synthesis. Creating such a set requires expert engineers and is difficult to maintain in a growing code-base. This work focuses on automatically discovering and proving lemmas, using a novel deductive approach. By using a deductive approach, terms can be represented by symbolic terms (where variables are universally quantified). Symbolic terms can then represent any object, whether it is a database or a function, without incurring long runtimes. The evaluation shows this method to be superior to prior-art both in run-time and in the lemmas collected.

Code

Augmented reality speech recognition for the hearing impaired

Speech to text software is a valuable tool for the hearing impaired. It enables them to attend lectures with real-time transcription.  A common issue in such lectures is the vocabulary where missing words will lead to errors in transcription. Speech to text techniques traditionally are built from three models, a physical model for processing sounds, a phonetic model to translate sounds to a phonetic word\sentence, and finally the language model. The language model translates the phonetics to words, using the vocabulary and some statistical model. By creating a custom vocabulary from Wikipedia we both get a relevant vocabulary and a context-aware statistical model which leads to a decrease in transcription error rate.

code

(some) Open Source Contributions

Rust Invariants

A repo for creating more meaningful integration tests and increase trust in the code base. This works by controlling asserts similar to logging such that production is not affected

Repo

Rust Process Function

In rust regular multithreading libraries do not provide a way to stop compute intensive threads. To overcome this, I created a macro repo to automatically create wrappers running in a new process.

Repo

Cap

Cap is a library to control memory usage in rust by overriding the global allocator and wrapping it. I contributed a statistics collection feature the repository.

Repo

Projects

Done as part of a summer internship or an academic project

github

Product Catagory prediction

@Oath

Deep learning model to predict product categories from short text description. Based on the recognition that categories are hierarchical to improve training time and prediction metrics.

Description Generation

@EBay

Automatically generating descriptions from key/value pairs. Based on both classic NLP methods for summarization and a deep learning model.

Stock price prediction

@Technion

Predicting stock price while attempting to capture market changes as a feature. The hypothesis is that there will be a time gap between changes in one market to the other which can be used.

Code

Code For Fun

Github

Shopping Bot

When the telegram bot API was published I wanted to check it out. I created a simple shopping list bot for me and my roommates. It was in the top 3 bots in the bot store for a while :)

Course Tree

There is a lot of flexibility in choosing which courses to take. In order to balance work and studying I created a simple tool to plan ahead, which courses are entailed by the current possibilities. This tool was later used by academic advisors in the Civil Engineering faculty.

GO TO
CODE
GO TO
Code