Title: Model Checking Abstract Plexil Programs with Smart