We conduct research to facilitate better reasoning about computational software, problems, and solutions. Our research advances the theory and practice of correct software development by leveraging concepts and techniques from logic, programming languages, and automated theorem proving.