Abstract We consider automated reasoning about recursively defined partial functions with decidable domain, i.e. functions computed by incompletely defined (or underspecified) but terminating functional programs. We define an interpreter for those programs, consider termination and investigate the semantics of incompletely defined programs. The interpreter may halt with a stuck computation, e.g. when dividing a number by zero, which represents a runtime error in a conventional programming environment. We show how so-called domain procedures are synthesized which decide the domain of incompletely defined procedures in almost all cases. As calls of domain procedures occur in proof obligations, domain procedures are optimized to make them as simple as possible. We also use domain procedures to refine the program semantics such that statements causing stuck computations do not hold. Our method to reason about incompletely defined programs is implemented in the verification tool .

We identify two faults in a published algorithm for fast computation of multiplicative inverses modulo prime powers. We patch the algorithm and present machine-assisted proofs of correctness of the repair. Our formal proofs also reveal that being prime is an unnecessary demand for the power base, thus attributing a wider scope of applications to the repaired algorithm.

We report on a machine assisted verification of an efficient implementation of Montgomery Multiplication which is a widely used method in cryptography for efficient computation of modular exponentiation. We shortly describe the method, give a brief survey of the VeriFun system used for verification, present the formal proofs and report on the effort for creating them. Our work uncovered a serious fault in a published algorithm for computing multiplicative inverses based on Newton-Raphson iteration, thus providing further evidence for the benefit of computer-aided verification.

Many-sorted unification is considered; that is, unification in the many-sorted free algebras of terms, where variables, as well as the domains and ranges of functions, are restricted to certain subsets of the universe, given as a potentially infinite hierarchy of sorts. It is shown that complete and minimal sets of unifiers may not always exist for many-sorted unification. Conditions for sort hierarchies that are equivalent for the existence of these sets with one, finitely many, or infinitely many elements are presented. It is also proved that being a forest-structured sort hierarchy is a necessary and sufficient criterion for the Robinson Unification Theorem to hold for many-sorted unification. An algorithm for many-sorted unification is given.