Most verification approaches assume a mathematical formalism in which functions
are total, even though partial functions occur naturally in many applications.
Furthermore, although there have been various proposals for
logics of partial functions, there is no consensus on which is "the right"
logic to use for verification applications.
In this paper, we propose using a three-valued Kleene logic,
where partial functions return the "undefined" value when applied outside of
their domains. The particular semantics are chosen according to the
*principle of least surprise* to the user; if there is disagreement among
the various approaches on what the value of the formula should be, its
evaluation is undefined. We show that the problem of checking validity in
the three-valued logic can be reduced to checking validity in a standard
two-valued logic, and describe how this approach has been successfully
implemented in our tool, CVC Lite.