Lev Naiman
Office: Bahen Centre 3232
Table of Contents
About Me
I am a PhD student at the Department of Computer Science at the University of Toronto. I am working under the supervision of Eric Hehner in the Software Engineering Group. I did both my undergraduate and Master's work at the University of Toronto.
Research Interests
My current work is on an interactive theorem prover called Netty. It is a theorem prover that uses direct manipulation as well as context and monotonicity to proceed with proofs. In addition, the prover can be used to develop code from specification using step-based refinement. My most recent efforts are more closely related to code synthesis; I am attempting to devise a method for code reuse based not just on single proof patterns, but rather whole specification lattices. As such, I am interested in:
- Interactive theorem provers
- Correct by construction programs
- Code synthesis and reuse
Publications
- L.Naiman, E.C.R.Hehner: Netty: a Prover's Assistant, COMPUTATION TOOLS 2011: the second international conference on Computational Logics, Algebras, Programming, Tools, and Benchmarking, Rome, 2011 September 25-30
- L.Naiman: Using an Expression Interpreter to Reason With Partial Terms COMPUTATION TOOLS 2013: the fourth international conference on Computational Logics, Algebras, Programming, Tools, and Benchmarking, Valencia, 2013 May 27- June 1
Presentations
- A tutorial in the iFM-ABZ 2012 conference on the Netty tool
Teaching
I have done TA work for the following courses
Links
- The Netty tool source code and project can be downloaded from here, and a compiled version in JAR format is here . It can be run by typing into console "java -jar netty.jar". The tool is still a work in progress and not feature-complete.
- The Netty document describes the tool
- A Practical Theorey of Programming by Eric Hehner describes the programming theory that Netty is based on.