Bitvector Support in the Theta Formal Verification Framework

The verification of safety-critical software systems has many challenges, such as the complex language constructs in embedded software. This paper addresses the verification problem of software systems using bitwise operations, and we present an extension to the Theta open-source formal verification framework. Our goal is to integrate bitvectors and bitwise operations in the abstraction-refinement...