Title: Model Checking Abstract PLEXIL Programs with SMART