Combination Methods for Software Verification

The thesis is devoted to the development of formal methods for software verification. Indeed, two are among the most widespread techniques that allow to rigorously specify the possible executions of a system and check whether it contains bugs. On the one hand, the correctness of a program can be guaranteed by showing the unsatisfiability of a formula modulo a theory which usually axiomatizes the involved datatypes; on the other hand, the model checking techniques are used to certify that every possible run of the system satisfies the desired properties. The contributions of the thesis are the following: First of all, we give a decidability result for the constraint satisfiability problem for interesting extensions of the theory of arrays. Secondly, along the lines of Manna and Pnueli, who have shown how a mixture of first-order logic and linear time temporal logic is sufficient to state the verification problems for the class of reactive systems, we draw on the recent literature about the combination of decision procedures to give decidability and undecidability results for the satisfiability problem for logics that allow to plug reasoning modulo first-order theories into a temporal setting. The results obtained in the case of linear flows of time are then generalized to the temporal and modal logics whose relativized satisfiability problem is decidable. The last contribution is the decidability of the model checking problem for linear flows of time under suitable hypothesis over the first-order theories involved. The proofs of the decidability results suggest that efficient Satisfiability Modulo Theories solvers might be successfully employed in the model checking of infinite-state systems.