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.
Contact Information
eytan.singher [at] gmail.com
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.
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.
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.
created with
Website Design Software .