aalta/aaltaf

Published in Software Engineering, ECNU, 2023

aalta is a SAT-based satisfiability checker for LTL over infinite traces, and aaltaf is for LTL over finite traces. In the long term, the two tools should be merged as one, but we are not done yet.

The aalta tool can be downloaded here.

The aaltaf tool can be downloaded here.