New version of ALASKA available !

Version 0.4 of Alaska has been released on May 12th. You can download it here.

ALASKA is a tool for the analysis of logic, automata, and symbolic kripke structures. Its main purpose is to demonstrate the usefulness of antichain-based techniques applied to model checking and temporal logic analysis.

About the tool

The ALASKA tool is an implementation of some of the theoretical results obtained by our research team. See the Antichain for Verification page for more details about antichain-based verification algorithms.

At the moment, ALASKA is able to perform the following :

• LTL satisfiability, validity and equivalence checking,
• Emptiness of alternating finite automata,
• Emptiness of alternating Buechi automata,
• Model checking of LTL on NuSMV models (LTLSPECs).

ALASKA is free software and is distributed under the terms of the GPLv2.

On this site, you can :

• Test Alaska using our server
• Download the tool for local use
• Get information on how to use Alaska
• Read about experimentations we made to compare the performance of Alaska to other tools
• Find the research papers where the theoretical background of Alaska can be found