{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:44Z","timestamp":1761611204385},"reference-count":26,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2007,8,1]],"date-time":"2007-08-01T00:00:00Z","timestamp":1185926400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2007,8]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We report on an experiment in combining the theorem prover Isabelle with automatic first-order arithmetic provers to increase automation on the verification of distributed protocols. As a case study for the experiment we verify several averaging clock synchronization algorithms. We present a formalization of Schneider\u2019s generalized clock synchronization protocol [Sch87] in Isabelle\/HOL. Then, we verify that the convergence functions used in two clock synchronization algorithms, namely, the Interactive Convergence Algorithm (ICA) of Lamport and Melliar-Smith [LMS85] and the Fault-tolerant Midpoint algorithm of Lundelius\u2013Lynch [LL84], satisfy Schneider\u2019s general conditions for correctness. The proofs are completely formalized in Isabelle\/HOL. We identify parts of the proofs which are not fully automatically proven by Isabelle built-in tactics and show that these proofs can be handled by automatic first-order provers with support for arithmetics.<\/jats:p>","DOI":"10.1007\/s00165-007-0027-6","type":"journal-article","created":{"date-parts":[[2007,5,2]],"date-time":"2007-05-02T15:12:11Z","timestamp":1178118731000},"page":"321-341","source":"Crossref","is-referenced-by-count":9,"title":["Verification of clock synchronization algorithms: experiments on a combination of deductive tools"],"prefix":"10.1145","volume":"19","author":[{"given":"Dami\u00e1n","family":"Barsotti","sequence":"first","affiliation":[{"name":"Universidad Nacional de C\u00f3rdoba, Ciudad Universitaria, 5000, C\u00f3rdoba, Argentina"}]},{"given":"Leonor Prensa","family":"Nieto","sequence":"additional","affiliation":[{"name":"LORIA, 54506, Vandoeuvre-l\u00e8s-Nancy, France"}]},{"given":"Alwen","family":"Tiu","sequence":"additional","affiliation":[{"name":"Research School of Information Sciences and Engineering, Australian National University and National ICT Australia, 0200, Canberra, ACT, Australia"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","unstructured":"Barsotti D (2006) Instances of schneider\u2019s generalized protocol of clock synchronization. In: Klein G Nipkow T Paulson L (eds) The archive of formal proofs. Formal proof development http:\/\/afp.sf.net\/entries\/ClockSynchInst.shtml"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Bishop S Fairbairn M Norrish M Sewell P Smith M Wansbrough K (2006) Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations. In: POPL\u201906: conference record of the 33rd ACM SIGPLAN-SIGACT symposium on principles of programming languages. ACM Press New York pp 55\u201366","DOI":"10.1145\/1111037.1111043"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Botaschanjan J Kof L K\u00fchnel C Spichkova M (2005) Towards verified automotive software. In: Proceedings of the 2nd international ICSE workshop on software. ACM Press New York","DOI":"10.1145\/1083190.1083199"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.10.005"},{"key":"e_1_2_1_2_5_2","unstructured":"CVC Lite. http:\/\/chicory.stanford.edu\/CVC\/"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Dennis LA Collins G Boulton R Slind K Robinson G Gordon M Melham T (2003) The PROSPER toolkit. In: Graf S Schwartzbach M (eds) Proceedings of TACAS\u201903 number 1785 in LNCS Springer Heidelberg pp 78\u201392","DOI":"10.1007\/3-540-46419-0_7"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"de Moura L (2004) SAL: Tutorial. Computer science laboratory SRI International","DOI":"10.1007\/978-3-540-27813-9_45"},{"key":"e_1_2_1_2_8_2","unstructured":"Consortium F (2004) FlexRay Communications System Protocol Specification Version 2.0"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Fontaine P Marion J-Y Merz S Nieto LP Tiu A (2006) Expressiveness + automation + soundness: towards combining smt solvers and interactive proof assistants. In: Holger H Jens P (eds) TACAS lecture notes in computer science Vol 3920. Springer Heidelberg pp 167\u2013181","DOI":"10.1007\/11691372_11"},{"key":"e_1_2_1_2_10_2","unstructured":"Isabelle home page. http:\/\/isabelle.in.tum.de\/"},{"key":"e_1_2_1_2_11_2","unstructured":"K\u00fchnel C Spichkova M (2006) FlexRay und FTCom: Formale Spezifikation in FOCUS. Technical report I0601 Technische Universit\u00e4t M\u00fcnchen"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Lundelius J Lynch N (1984) A new fault-tolerant algorithm for clock synchronization. In: Proceedings of PODC \u201984. ACM Press New York pp 75\u201388","DOI":"10.1145\/800222.806738"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/2455.2457"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.12.005"},{"key":"e_1_2_1_2_15_2","unstructured":"Miner PS (1993) Verification of fault-tolerant clock synchronization systems. NASA technical paper 3349 NASA Langley Research Center"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Meng J Paulson LC (2004) Experiments on supporting interactive proof using resolution. In: Basin DA Rusinowitch M (eds) IJCAR lecture notes in computer science Vol 3097. Springer Heidelberg pp 372\u2013384","DOI":"10.1007\/978-3-540-25984-8_28"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Nipkow T (2002) Structured proofs in Isar\/HOL. In: Geuvers H Wiedijk F (eds) TYPES lecture notes in computer science Vol 2646. Springer Heidelberg pp 259\u2013278","DOI":"10.1007\/3-540-39185-1_15"},{"key":"e_1_2_1_2_18_2","unstructured":"Ranise S Tinelli C (2005) The SMT-LIB standard : Version 1.1"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Siekmann JH Benzm\u00fcller C Brezhnev V Cheikhrouhou L Fiedler A Franke A Horacek H Kohlhase M Meier A Melis E Moschner M Normann I Pollet M Sorge V Ullrich C Wirth C-P Zimmer J (2002) Proof development with OMEGA. In: CADE pp 144\u2013149","DOI":"10.1007\/3-540-45620-1_12"},{"key":"e_1_2_1_2_20_2","unstructured":"Schneider FB (1987) Understanding protocols for Byzantine clock synchronization. Technical report TR 87\u2013859 Cornell University"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Shankar N (1992) Mechanical verification of a generalized protocol for byzantine fault tolerant clock synchronization. In: Vytopil J (ed) Formal techniques in real-time and fault-tolerant systems lecture notes in computer science Vol 571. Springer Nijmegen pp 217\u2013236","DOI":"10.1007\/3-540-55092-5_12"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Schwier D von Henke F (1998) Mechanical verification of clock synchronization algorithms. In: Ravn AP Rischel H (eds) Formal techniques in real-time and fault-tolerant systems number 1486 in LNCS. Springer Heidelberg pp 262\u2013271","DOI":"10.1007\/BFb0055353"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.5555\/2773566.2773663"},{"key":"e_1_2_1_2_24_2","unstructured":"Tiu A (2005) A formalization of a generalized clock synchronization protocol in Isabelle\/HOL. In: Klein G Nipkow T Paulson L (eds) The archive of formal proofs. http:\/\/afp.sf.net\/entries\/GenClock.shtml Formal proof development"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.12.007"},{"key":"e_1_2_1_2_26_2","unstructured":"Yices home page. http:\/\/fm.csl.sri.com\/yices\/"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-007-0027-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-007-0027-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-007-0027-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:45:16Z","timestamp":1641483916000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-007-0027-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,8]]},"references-count":26,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2007,8]]}},"alternative-id":["10.1007\/s00165-007-0027-6"],"URL":"https:\/\/doi.org\/10.1007\/s00165-007-0027-6","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,8]]}}}