Deciding Fixed and Non-fixed Size Bit-vectors. - Nikolaj S. Bjørner; Mark C. Pichora (TACAS, 1998)

An Update on STeP: Deductive-Algorithmic Verification of Reactive Systems. - Zohar Manna; Nikolaj S. Bjørner; Anca Browne; Michael Colón; Bernd Finkbeiner; Mark C. Pichora; Henny B. Sipma; Tomás E. Uribe (Tool Support for System Specification, Development and Verification, 1998)