UCLID ( /ˈjuːklɪd/, the same as "Euclid") is a decision procedure for CLU logic and can be used as a tool for bounded model checking of infinite-state systems.
Read more about Uclid: Decision Procedure and Verification Tool, People, Beaver – Decision Procedure For Bit-vector Arithmetic