Loading...
Please wait, while we are loading the content...
Similar Documents
Towards a Combination of Heterogeneous Deductive Tools for System Verification : A Case Study on Clock Synchronization
| Content Provider | Semantic Scholar |
|---|---|
| Author | Fontaine, Pascal Gupta, Kamal Kant Marion, Jean-Yves Merz, Stephan Nieto, Leonor Prensa Tiu, Alwen |
| Copyright Year | 2005 |
| Abstract | For formal system verification to become common practice, it has to be supported by flexible and powerful deductive tools that can accommodate adequate levels of abstraction as well as a high degree of automation. In this paper, we report on a case study on combination of deductive tools to support verification of distributed algorithms. More specifically, we verify several clock synchronization algorithms using an interactive proof assistant, in combination with several arithmetic and SAT solvers. Our initial finding has been positive; the use of automated provers helps solving a significant part of the verification problem that deals with real arithmetics (which cannot be handled by the proof assistant) and first-order reasoning. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://qsl.loria.fr/groupeplateforme/pubs/appsem05proc.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
