Linked Presentation: Automated Reasoning and Detection of Specious Configuration in Large Systems with Symbolic Execution