The PlusCal Algorithm Language

1. Wirth, N.: Algorithms + Data Structures = Programs. Prentice-Hall, Englewood Cliffs (1975)

   MATH  Google Scholar 

2. Lamport, L.: Specifying Systems. Addison-Wesley, Boston (2003), http://lamport.org

   MATH  Google Scholar 

3. Yu, Y., Manolios, P., Lamport, L.: Model checking TLA⁺ specifications. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 54–66. Springer, Heidelberg (1999)

   Chapter  Google Scholar 

4. Lamport, L.: The PlusCal algorithm language, http://research.microsoft.com/users/lamport/tla/pluscal.html The page can also be found by searching the Web for the 25-letter string obtained by removing the “-” from uid-lamportpluscalhomepage

5. Sedgewick, R.: Algorithms. Addison-Wesley, Reading (1988)

   MATH  Google Scholar 

6. Hoare, C.A.R.: Algorithm 64: Quicksort. Communications of the ACM 4, 321 (1961)

   Article  Google Scholar 

7. Lamport, L.: A fast mutual exclusion algorithm. ACM Transactions on Computer Systems 5, 1–11 (1987)

   Article  Google Scholar 

8. Lamport, L.: What good is temporal logic? In: Mason, R.E.A. (ed.) Information Processing 83: Proceedings of the IFIP 9th World Congress, Paris, IFIP, pp. 657–668. North-Holland, Amsterdam (1983)

   Google Scholar 

9. Pratt, V.R.: Semantical considerations on Floyd-Hoare logic. In: 17th Symposium on Foundations of Computer Science, pp. 109–121. IEEE, Los Alamitos (1976)

   Google Scholar 

10. Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann, San Mateo (1995)

    Google Scholar 

11. Francez, N.: Fairness. Texts and Monographs in Computer Science. Springer, Heidelberg (1986)

    Google Scholar 

12. Lamport, L.: Checking a multithreaded algorithm with ⁺CAL. In: Dolev, S. (ed.) DISC 2006. LNCS, vol. 4167, pp. 151–163. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

13. Lamport, L.: The temporal logic of actions. ACM Transactions on Programming Languages and Systems 16, 872–923 (1994)

    Article  Google Scholar 

14. Schwartz, J.T., Dewar, R.B., Schonberg, E., Dubinsky, E.: Programming with sets: An Introduction to SETL. Springer, New York (1986)

    Book  MATH  Google Scholar 

15. Jackson, D.: Alloy: a lightweight object modelling notation. ACM Transactions on Software Engineering and Methodology 11, 256–290 (2002)

    Article  Google Scholar 

16. Holzmann, G.J.: The Spin Model Checker. Addison-Wesley, Boston (2004)

    Google Scholar 

17. McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)

    Book  MATH  Google Scholar 

18. Gurevich, Y.: Can abstract state machines be useful in language theory? Theoretical Computer Science 376, 17–29 (2007)

    Article  MathSciNet  MATH  Google Scholar 

19. Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)

    MATH  Google Scholar 

20. Hoare, C.A.R.: Communicating sequential processes. Communications of the ACM 21, 666–677 (1978)

    Article  MATH  Google Scholar 

Download references