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 :
Theses
Complete list of metadatas

Cited literature [139 references]  Display  Hide  Download

https://hal.univ-lorraine.fr/tel-01748341
Contributor : Thèses Ul <>
Submitted on : Thursday, March 29, 2018 - 11:32:10 AM
Last modification on : Tuesday, April 24, 2018 - 1:53:20 PM
Long-term archiving on : Friday, September 14, 2018 - 12:56:52 AM

File

SCD_T_2008_0006_ZUCCHELLI.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : tel-01748341, version 1

Collections

Citation

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

Share

Metrics

Record views

30

Files downloads

28