Skip to Main content Skip to Navigation
New interface

Combination methods for software verification

Abstract : 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, 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, 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 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 verification problems for the class of reactive systems, we draw on the recent literature about 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 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.
Document type :
Complete list of metadata

Cited literature [139 references]  Display  Hide  Download
Contributor : Thèses UL Connect in order to contact the contributor
Submitted on : Thursday, March 29, 2018 - 11:32:10 AM
Last modification on : Saturday, October 16, 2021 - 11:26:08 AM
Long-term archiving on: : Friday, September 14, 2018 - 12:56:52 AM


Files produced by the author(s)


  • HAL Id : tel-01748341, version 1



Daniele Zucchelli. Combination methods for software verification. Other [cs.OH]. Université Henri Poincaré - Nancy 1, 2008. English. ⟨NNT : 2008NAN10006⟩. ⟨tel-01748341⟩



Record views


Files downloads