I have contributed to the development of a number of tools, some of them are listed below. Please contact me if you have problems or if you want to know more, don’t be afraid! I normally reply very quickly if I am in front of the PC. Also, I have other code that is described in my papers, if you don’t find it here, again, simply send me an email and I’ll be happy to reply.

  • MCMAS:  this is a tool for symbolic model checking multi-agent systems developed in conjunction with Alessio Lomuscio and Hongyang Qu.
  • Mc-COGWED: a prototype model checker for COGWED (a COmputationally Grounded, wEighted Doxastic logic).
  • jpf-bdd: this is an extension of Java Pathfinder (JPF) that uses Binary Decision Diagrams (BDDs) to represent and explore parts of the state space of a Java program symbolically. It was developed for Google Summer of Code 2011 in conjunction with Alexander von Rehin.
  • jpf-ltl: this is an extension of Java Pathfinder (JPF) that enables the verification of LTL properties of Java programs. It is currently being developed in conjunction with Michele Lombardi (University of L’Aquila).
  • this is a tool to create simple multiple-choice questions for my lectures, developed in conjunction with Lalith Kaushik.
  • pddleditor_1.0.0.jar: this is an Eclipse plug-in to edit PDDL (Planning Domain Definition Language) files and to automatically generate test cases from temporal requirements.
  • this is an Eclipse plug-in to generate Axis monitors from Service Level Agreements written in SLAng. The installation can be complicated, contact me for help.

“La teoria è sapere come funzionano le cose e non sapere come farle funzionare; la pratica è sapere come far funzionare la cose senza sapere come funzionano; il nostro scopo è unire la pratica alla teoria per riuscire a non far funzionare le cose senza capire come abbiamo fatto”