Abstraction and modular reasoning for the verification of software

Modern software systems, which are often concurrent and distributed, must be extremely reliable and correct. Finite-state verification (FSV) techniques, such as model checking, are emerging as the front-runner in the race to automate high-quality assurance of software. Such techniques exhaustively check a finite-state model of a system for violations of system requirements stated in a complementary formalism, such as assertions or temporal logic formulae.; This thesis will address several of the challenges of building finite-state models of software systems, that are amenable to verification using existing FSV tools.; First, the existence of very large or infinite data in software, that comes from (potentially) unbounded data types, makes FSV of software difficult. We consider one method for avoiding this problem: tool support for source-to-source to small finite domains.; Second, most FSV tools are aimed at reasoning about complete systems, but modern software is, increasingly, built as a collection of independently produced components, which are assembled to achieve a system's requirements. We will describe an automatic technique for building finite-state models of software components that are amenable to FSV using existing tools. The technique enables modular reasoning about software components, taking into account assumptions about the behavior of the environment in which the components will execute.; We will illustrate the application of our approach to FSV of software on several large case studies, written in Ada and Java.