×
Barsotti, Damián; Nieto, Leonor Prensa; Tiu, Alwen

Verification of clock synchronization algorithms: experiments on a combination of deductive tools. (English) Zbl 1125.68107

Formal Asp. Comput. 19, No. 3, 321-341 (2007).

Cited in 5 Documents

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68Q60 Specification and verification (program logics, model checking, etc.)

Keywords:

Theorem proving; Verification; Clock synchronization; Combination of deductive tools

Citations:

Zbl 0629.68025; Zbl 0646.68029

Software:

SMT-LIB; CVC Lite; HOL Light; PROSPER; Isabelle/HOL; Prosper; Isabelle; Isar; TPTP; Schneider clock synchronization; Yices; Calife; Archive Formal Proofs; clock synchronization
Cite Review PDF
Full Text: DOI Link

References:

[1] Barsotti D (2006) Instances of schneider’s 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
[2] 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’06: conference record of the 33rd ACM SIGPLAN-SIGACT symposium on principles of programming languages. ACM Press, New York, pp 55–66
[3] Botaschanjan J, Kof L, Kühnel C, Spichkova M (2005) Towards verified automotive software. In: Proceedings of the 2nd international ICSE workshop on software. ACM Press, New York
[4] Barsotti D, Nieto LP, Tiu A (2006) Verification of clock synchronization algorithms: experiments on a combination of deductive tools. Electr Notes Theor Comput Sci 145:63–78 · doi:10.1016/j.entcs.2005.10.005
[5] CVC Lite. http://chicory.stanford.edu/CVC/
[6] 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’03, number 1785 in LNCS, Springer, Heidelberg, pp 78–92 · Zbl 0971.68638
[7] de Moura L (2004) SAL: Tutorial. Computer science laboratory, SRI International
[8] Consortium F (2004) FlexRay Communications System Protocol Specification Version 2.0
[9] 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–181 · Zbl 1180.68240
[10] Isabelle home page. http://isabelle.in.tum.de/
[11] Kühnel C, Spichkova M (2006) FlexRay und FTCom: Formale Spezifikation in FOCUS. Technical report I0601, Technische Universität München
[12] Lundelius J, Lynch N (1984) A new fault-tolerant algorithm for clock synchronization. In: Proceedings of PODC ’84. ACM Press, New York, pp 75–88 · Zbl 0591.68023
[13] Lamport L, Melliar-Smith PM (1985) Synchronizing clocks in the presence of faults. J ACM 32(1):52–78 · Zbl 0629.68025 · doi:10.1145/2455.2457
[14] McLaughlin S, Barrett C, Ge Y (2006) Cooperating theorem provers: A case study combining hol-light and cvc lite. Electr. Notes Theor. Comput. Sci. 144(2):43–51 · Zbl 1272.68362
[15] Miner PS (1993) Verification of fault-tolerant clock synchronization systems. NASA technical paper 3349, NASA Langley Research Center
[16] 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–384 · Zbl 1126.68574
[17] 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–278 · Zbl 1023.68657
[18] Ranise S, Tinelli C (2005) The SMT-LIB standard : Version 1.1
[19] Siekmann JH, Benzmüller 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–149 · Zbl 1072.68591
[20] Schneider FB (1987) Understanding protocols for Byzantine clock synchronization. Technical report TR 87–859, Cornell University
[21] 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–236
[22] 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–271
[23] Tavernier B (2004) Calife: a generic graphical user interface for automata tools. Electr Notes Theor Comput Sci 110:169–172a · doi:10.1016/j.entcs.2004.06.004
[24] 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
[25] Weber T (2006) Integrating a SAT solver with an LCF-style theorem prover. Electr Notes Theor Comput Sci 144(2):67–78 · doi:10.1016/j.entcs.2005.12.007
[26] Yices home page. http://fm.csl.sri.com/yices/
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.