Title: Using Differential Formal Analysis for dependable number entry User interfaces that employ the same display and buttons may look the same but can work very differently depending on how they are implemented. In healthcare, it is critical that interfaces that look the same are the same. Hospitals typically have many types of similar infusion pumps, with different software versions, and variation between pump behavior may lead to unexpected adverse events. For example, when entering drug doses into infusion pumps that use the same display and button designs, different results may arise when pushing identical sequences of buttons. These differences are a result of subtle implementation differences and may lead to under-dose or over-dose errors. This seminar explores different implementations of a 5-key interface for entering numbers using a new user interface analysis technique, Differential Formal Analysis. Using Differential Formal Analysis different 5-key interfaces are analyzed based on log data collected from 19 infusion pumps over a 3 year period from a UK hospital. A comparison is made between domain specific results and generic results from Differential Formal Analysis performed using random data.