Time-Aware Abstractions in HybridSal

re Abstractions in HybridSal Ashish Tiwari SRI International, Menlo Park, CA Abstract. HybridSal is a tool for enabling verification of hybrid systems using infinite bounded model checking and k-induction. The core t of the tool is an abstraction engine that automatically creates a discrete, but infinite, state transition system abstraction of the continuous dynamics in the system. In this paper, we describe HybridSal’s new ty to create time-aware relational abstractions, which gives users over the precision of the abstraction. We also describe a novel for abstracting nonlinear expressions that allows us to create time-aware relational abstractions that are more precise than those described previously. We show that the new approach enables automatic verification of systems that could not be verified previously.

• Type: Journal
• Year: 2015
• Where: CAV
• Authors: Ashish Tiwari
• Keywords: CAV 2015, Hardware