Jacco

Overview

Jacco is a toolset for model checking of Java actor programs. Jacco currently supports actor programs written in ActorFoundry Library. It generates the state space of a given program and performs analysis against safety properties (assertion-based model checking). In order to perform model checking without modifying source codes, some modifications have been made to ActorFoundry library and the result is uploaded here.