BAT: The Bit-Level Analysis Tool

Abstract. While effective methods for bit-level verification of low-level properties exist, system-level properties that entail reasoning about a significant part of the design pose a major verification challenge. We present the Bit-level Analysis Tool (BAT), a state-of-the-art decision procedure for bit-level reasoning that implements a novel collection of techniques targeted towards enabling the verification of system-level properties. Key features of the BAT system are an expressive strongly-typed modeling and specification language, a fully automatic

• Type: Conference
• Year: 2007
• Where: CAV
• Authors: Panagiotis Manolios, Sudarshan K. Srinivasan, Daron Vroon
• Keywords: CAV 2007, Formal Methods