Tool homepage: http://alpina.unige.ch/
Tool availability: Free of charge
AlPiNA is implemented as an Eclipse plugin. The user interface was created using the EMP metamodeling approach. Thus, models are easy to implement, without the need to know the underlying techniques related to model checking performance.
The actual model checking is performed in an independent engine, implemented in Java. It performs symbolic model checking based on ΣDD, an eﬃcient evolution in the Decision Diagrams ﬁeld, using novel techniques such as algebraic clustering and algebraic unfolding. This allows to check models with very large state spaces.
Prof. Didier Buchs Computer Science Department University of Geneva 7 route de Drize, B‚t. A, CH-1227 Carouge Switzerland Phone: 0041 22 37 90 161 Fax: 0041 22 37 90 250 E-mail: email@example.com