L12 (10.24): Model checkers and applications