Welcome !

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 :