Amin Bandali

Dept. Of Electrical Engineering & Computer Science



Amin Bandali is a 4th year Computer Science student at the Lassonde School of Engineering, York University. Amin's research interests are programming languages and formal methods. Specifically, functional programming languages, type systems, proof systems, and automated provers. Amin spent the last summer in the Software Engineering Lab under supervision of Professor Jonathan Ostroff and Simon Hudon, working on various parts of the Literate Unit-B theorem prover and creating Unit-B Web. Unit-B is a new formal framework for specifying and modeling systems that must satisfy both safety and liveness properties. Literate Unit-B is the tooling that supports the Unit-B Logic and Unit-B's computation models. Unit-B Web is a web interface for doing predicate calculus proofs, bringing the Literate Unit-B prover to the web.


The Magic of Specifications and Type Systems
Writing specifications for complex software is as important as blueprints are for skyscrapers and bridges that are safe and fit for their purpose. The aim of this project is taking a step towards making writing specifications for software more readily and more easily accessible by taking advantage of the power of theorem provers and type systems.

For this, I built Unit-B Web, a web interface for doing predicate calculus proofs. Unit-B is a new formal framework for specifying and modeling systems that must satisfy both safety and liveness properties. Its back-end written in Haskell and its front-end in the JavaScript programming language, Unit-B Web supports the logic of Unit-B and makes it available in the browser.

Unit-B Web leverages the power of the Z3 theorem prover along with its own type checker to two purposes:

1. Teaching: Unit-B Web can be used in classroom for demonstrations, or for evaluation in form of assignments or online quizzes (by integrating into department's online quiz system), and
2. online proof environment: making tooling for set theory, functions, relations, arithmetic, intervals, and predicate calculus theories available on the web, Unit-B Web serves as a proof of concept for a web IDE.

Logic is fulfilling more and more the promise of aiding computer scientists and software engineers develop more reliable software, by enabling them to work at a more abstract level by writing more concise specifications. The goal of Unit-B Web has been to help make specifications more accessible to casual users.

In near future, I will be revamping Unit-B Web and extending its feature set to bring it on a par with Unit-B's main tooling, Literate Unit-B, supporting the modeling capabilities of Unit-B and serving as an easily accessible proof environment.