L12: Model checkers and applications