The PlusCal algorithm language. Algorithms are different from programs and should not be described with programming languages. The only simple alternative to programming languages has been pseudo-code. PlusCal is an algorithm language that can be used right now to replace pseudo-code, for both sequential and concurrent algorithms. It is based on the TLA + specification language, and a PlusCal algorithm is automatically translated to a TLA + specification that can be checked with the TLC model checker and reasoned about formally.
Keywords for this software
References in zbMATH (referenced in 7 articles )
Showing results 1 to 7 of 7.
- Chevrou, Florent; Hurault, Aurélie; Quéinnec, Philippe: On the diversity of asynchronous communication (2016)
- Methni, Amira; Lemerre, Matthieu; Ben Hedia, Belgacem; Haddad, Serge; Barkaoui, Kamel: Specifying and verifying concurrent C programs with TLA+ (2015) ioport
- Gmeiner, Annu; Konnov, Igor; Schmid, Ulrich; Veith, Helmut; Widder, Josef: Tutorial on parameterized model checking of fault-tolerant distributed algorithms (2014)
- Akhtar, Sabina; Merz, Stephan; Quinson, Martin: A high-level language for modeling algorithms and their properties (2011)
- Lamport, Leslie: Byzantizing Paxos by refinement (2011)
- Aguilera, Marcos K.; Gafni, Eli; Lamport, Leslie: The mailbox problem (2010)
- Lamport, Leslie: The PlusCal algorithm language (2009)