SHF: Small: Strengthening Correctness of Date and Time Logic in Software Systems

In software engineering, date and time are fundamental concepts. Whether it is scheduling flights, processing bank transactions, computing payroll wages, validating digital certificates, controlling industrial processes, or logging operational data—software relies heavily on making accurate calculations related to dates and times. However, code related to date and time calculations is often also a source of human error, due to the inherent complexity of concepts such as calendars, time zones, and daylight savings, as well as the wide variety of textual representations and international conventions used across different industries.

Moreover, most software makes use of third-party components, called libraries, for providing functionality related to date and time. Errors in any of these components can potentially impact the reliability of a huge number of software systems which depend on their correctness for day-to-day operations. This project aims to first systematically study past software bugs related to date and time computation by analyzing source code repositories, and then, to develop techniques for automatically uncovering new date and time related errors that may be present in existing software.

Successful completion of this project will improve software systems that our society critically relies on against a pervasive class of errors. The research project will also result in materials that will be incorporated in software engineering courses. At the same time, the project will provide research opportunities for undergraduate students and students from underrepresented groups in computing.

Consistently performing date/time computations accurately is challenging due to: (i) fundamental complexities with the domain such as dealing with leap years, time zones, daylight savings, clock drifts, diverse data representations and string formats, etc.; and (ii) the heterogeneous landscape of date/time interfaces across different programming languages and third-party libraries, which all provide similar functionality but use subtly different representations, conventions, and default behavior. This project aims to strengthen the correctness of date and time computations performed in software systems via: (i) a systematic study of date/time-related issues in open-source repositories; (ii) the development of static and dynamic program analysis techniques to uncover date and time bugs in open-source date/time libraries, as well as client software that makes use of such libraries; and (ii) enhancing support for formal reasoning of date-based constraints in theorem provers.

This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.