Software and Learning Materials



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.

Concurrent and distributed programming

  • DAJ is an interactive tool for studying distributed algorithms.
  • jBACI is a concurrency simulator with an integrated development environment.
  • Source code for How to Solve the Santa Claus Problem, Concurrency: Practice & Experience 10(6), 1998, 485-496.
  • Source code for Implementing Concurrency Using Inheritance, SIGCSE Bulletin 28(1), 1996, p. 180-184.

Java programming

Learning materials in English

Learning materials in Hebrew

Student projects (not supported)

  • Mikko Vinni. An incremental viewer of Dot graphs.
  • Trishank Karthik Kuppusamy. Pomegranate: A Compiler for Promela.
  • Maxim Mozgovoy. CPV: Concurrent Program Verifier.
  • Yakov Persky. SimAda Concurrency Simulator.
  • Yoav Tzruya. A Distributed Programming Environment for Ada95.
  • Shawn Silverman. DPLab: An environment for distributed programming.
  • CP: A Concurrency Simulator.