SAT based Verification Tool for Labeled Transition System

Multi-threaded Java programming such as an internet server program is difficult, because it is hard to detect subtle errors within multi-threading. LTSA is a too/for modeling and analyzing for catching some kinds of thread bugs, but still there remains scalability problem to deal with bigger applications. In this paper, we introduce a SAT based verification tool for Labeled Transition System and we explain LTS semantics and their CNF encoding. To verify large model, we focus our attention on efficient encoding for given model. In our tool, the property to be checked is expressed by either LTS or LTL formula based on Fluent. In order to solve a problem, LTSs and property are represented with CNF formulae, the input format to SAT-solver.