TLC is a model checker for specifications written in TLA+. TLA+ is a specification language based on TLA, the Temporal Logic of Actions. See the TLA web page for general information about TLA. You will most likely want to use TLC from the TLA Toolbox. Downloading the Toolbox brings with it the latest version of all the TLA+ tools, including TLC. How to write TLA+ specifications is explained in Specifying Concurrent Systems , which also describes TLC. However, it doesn’t tell you how to use the Toolbox.

References in zbMATH (referenced in 12 articles )

Showing results 1 to 12 of 12.
Sorted by year (citations)

  1. Smith, Graeme: Model checking simulation rules for linearizability (2016)
  2. Akhtar, Sabina; Merz, Stephan; Quinson, Martin: A high-level language for modeling algorithms and their properties (2011)
  3. Leuschel, Michael; Bendisposto, Jens: Directed model checking for B: an evaluation and new techniques (2011)
  4. Leuschel, Michael; Falampin, Jérôme; Fritz, Fabian; Plagge, Daniel: Automated property verification for large scale B models with ProB (2011) ioport
  5. Roh, Hyun-Gul; Jeon, Myeongjae; Kim, Jin-Soo; Lee, Joonwon: Replicated abstract data types: building blocks for collaborative applications (2011)
  6. Aguilera, Marcos K.; Gafni, Eli; Lamport, Leslie: The mailbox problem (2010)
  7. Zhang, Hehua; Merz, Stephan; Gu, Ming: Specifying and verifying PLC systems with (TLA^+) : a case study (2010) ioport
  8. Chaouch-Saad, Mouna; Charron-Bost, Bernadette; Merz, Stephan: A reduction theorem for the verification of round-based distributed algorithms (2009)
  9. Masalagiu, Cristian; Chin, Wei-Ngan; Andrei, Ştefan; Alaiba, Vasile: A rigorous methodology for specification and verification of business processes (2009)
  10. Regnier, Paul; Lima, George; Andrade, Aline: A TLA+ formal specification and verification of a new real-time communication protocol (2009)
  11. Win, Toh Ne; Ernst, Michael D.; Garland, Stephen J.; Kırlı, Dilsun; Lynch, Nancy A.: Using simulated execution in verifying distributed algorithms (2004) ioport
  12. Mokkedem, Abdel; Leonard, Tim: Formal verification of the Alpha 21364 network protocol (2000)