about ME

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

Researching new methods for automatic theory and their applications. Focusing on theory exploration for all underlying theories with the goal of applying these new tools in methods for program verification and synthesis.

read more

Contact Information

 ‚Äč eytan.singher [at] gmail.com

linkedin page


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.


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.



Done as part of a summer internship or an academic project

Product Catagory prediction


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


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

Stock price prediction


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 For Fun


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.