Automated Software Verification with First-Order Theorem Provers

Automating formal methods is an ongoing effort in software verification necessary to conclusively prove that critical software infrastructure is error-free. Applications such as IoT, cloud computing and blockchain show that bugs can have severe implications on the safety and security of software. In this thesis, we propose trace logic to automate deductive verification of software using first-order theorem proving. Automated reasoning in trace logic helps to prove safety properties of while-like programs in full first-order logic with support for theories and sorts. Our aim is to extend the logical expressiveness of program semantics in trace logic, offering a fully automated and scalable approach towards reasoning-based software verification. Specifically, our project extends reasoning with trace logic to interprocedural analysis and concurrency to make automated verification of these technologies possible and thereby pushing the state-of-the-art in automated reasoning.