Abstract
We report our experiences to verify distributed algorithms in constructive type theory by testing and proving. Properties can be tested to eliminate bugs before proving, thus saving expensive proof effort. Both deadlock property and liveness property are proven after testing. The verified algorithm can be executed in Cayenne, a functional programming language with dependent types.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Augustsson, L.: Cayenne: a language with dependent types. In: Berman, M., Berman, S. (eds.) ICFP 1998. Proceedings of the third ACM SIGPLAN International Conference on Functional Programming. ACM SIGPLAN Notices, vol. 34, 1, pp. 239–250. ACM Press, New York (1998)
Berghofer, S., Nipkow, T.: Random testing in Isabelle/HOL. In: Cuellar, J., Liu, Z. (eds.) SEFM 2004. Software Engineering and Formal Methods, IEEE Computer Society Press, Los Alamitos (2004)
Chou, C.-T.: Mechanical verification of distributed algorithms in higher-order logic. In: Melham, T.F., Camilleri, J. (eds.) Higher Order Logic Theorem Proving and Its Applications. LNCS, vol. 859, pp. 158–176. Springer, Heidelberg (1994)
Chandy, K.M., Misra, J.: The drinking philosopher’s problem. ACM Transactions on Programming Languages and Systems 6(4), 632–646 (1984)
Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell programs. In: ICFP 2000. Proceedings of the ACM SIGPLAN International Conference on Functional Programming, NY, september 18–21, 2000. ACM Sigplan Notices, vol. 35.9, pp. 268–279. ACM Press, New York (2000)
Coquand, C.: The Agda homepage, http://www.cs.chalmers.se/~catarina/agda
Coquand, T.: Inductive definitions and type theory: an introduction, http://www-sop.inria.fr/certilab/types-sum-school02/Lnotes/
Coquand, T., Pollack, R., Takeyama, M.: A logical framework with dependently typed records. In: Hofmann, M.O. (ed.) TLCA 2003. LNCS, vol. 2701, pp. 105–119. Springer, Heidelberg (2003)
Cover - combining verification methods in software development, http://www.coverproject.org/
Dybjer, P.: Inductive families. Formal Aspects of Computing 6(4), 440–465 (1994)
Dybjer, P., Haiyan, Q., Takeyama, M.: Random generators for dependent types. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol. 3407, pp. 341–355. Springer, Heidelberg (2005)
Dybjer, P., Haiyan, Q., Takeyama, M.: Combining testing and proving in dependent type theory. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, Springer, Heidelberg (2003)
Dybjer, P., Setzer, A.: A finite axiomatization of inductive and inductive-recursive definitions. In: Girard, J.-Y. (ed.) TLCA 1999. LNCS, vol. 1581, pp. 129–146. Springer, Heidelberg (1999)
Dybjer, P., Setzer, A.: Indexed induction-recursion. In: Kahle, R., Schroeder-Heister, P., Stärk, R.F. (eds.) PTCS 2001. LNCS, vol. 2183, Springer, Heidelberg (2001)
Groote, J.F., Monin, F., van de Pol, J.: Checking verifications of protocols and distributed systems by computer. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 629–655. Springer, Heidelberg (1998)
Hallgren, T.: The Alfa homepage, http://www.cs.chalmers.se/~hallgren/Alfa
Hayashi, S., Nakano, H.: PX, a Computational Logic. MIT Press, Cambridge (1988)
Hayashi, S., Sumitomo, R., Shii, K.-i.: Towards animation of proofs - testing proofs by examples. Theoretical Computer Science 272, 177–195 (2002)
Nordström, B., Petersson, K., Smith, J.M.: Programming in Martin-Löf type theory: an introduction. Oxford University Press, Oxford (1990)
Programatica: Integrating programming, properties, and validation, http://www.cse.ogi.edu/PacSoft/projects/programatica/
Vaandrager, F.W.: Verification of a distributed summation algorithm. In: Apt, K.R., Schrijver, A., Temme, N.M. (eds.) From Universal Morphisms to Megabytes – a Baayen Space Odyssey, Amsterdam, pp. 593–608. CWI (1994)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Haiyan, Q. (2007). Testing and Proving Distributed Algorithms in Constructive Type Theory. In: Gurevich, Y., Meyer, B. (eds) Tests and Proofs. TAP 2007. Lecture Notes in Computer Science, vol 4454. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73770-4_5
Download citation
DOI: https://doi.org/10.1007/978-3-540-73770-4_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73769-8
Online ISBN: 978-3-540-73770-4
eBook Packages: Computer ScienceComputer Science (R0)