Logic and model checking
- LearnSAT: A Prolog implementation of the DPLL algorithm for SAT solving, including conflict-directed clause-learning and non-chronological backtracking.
- jSpin is a simple integrated development environment for the Spin model checker.
- Erigone is a partial reimplementation of the Spin model checker intended to facilitate learning concurrency and model checking.
- VN is a tool for visualization of nondeterministic finite automata.
- Sokoban Solver in Promela. Download from GitHub: https://github.com/motib/sokoban-promela.
Concurrent and distributed programming
- DAJ is an interactive tool for studying distributed algorithms.
- jBACI is a concurrency simulator with an integrated development environment.
The Jeliot program animation system was developed in collaboration with Erkki Sutinen of the University of Joensuu, Finland (currently, the University of Eastern Finland). The work by carried out by many graduate students: Niko Myller, Ronit Ben-Bassat Levi, Roman Bednarik, Andres Moreno-Garcia, Gil Ebel.
- Learning Objects for Visualizations: Programming in Java Using Jeliot.
- Reference list of Jeliot commands (in Hebrew).
- SyntaxTrain: visualization of Java syntax errors.
- Compile and Runtime Errors in Java (PDF, LaTeX).