Uclid

Uclid

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.