SPLAT: A Tool for Model-Checking and Dynamically-Enforcing Abstractions