TLA+ | The way to specify

The TLA+ and PlusCal Resource

Skip to content

Search for:

Source code checked in, #c956032211a6db0d2cf38aa37ed900458d2b0a23 January 8, 2015
Source code checked in, #52b6333b1724dd51be51be5d142a341ff6d3af65 January 8, 2015
Source code checked in, #61fcdc8ad41a9908be846d4d4d92c35537b58c6e January 8, 2015
Source code checked in, #38ecd98988d60a7b8001a6449c36849694032154 January 8, 2015
Source code checked in, #5cc8cf4fbbaea17b440b44db3e3b304176add689 January 8, 2015

Created Unassigned: SANY accepts step names in DEF references (15-01-19) [34] January 20, 2015
Commented Issue: 12-10-05_1 : named instantiations with parameters [12] January 19, 2015
Edited Issue: 12-10-05_1 : named instantiations with parameters [12] January 19, 2015
Edited Issue: 12-10-05_1 : named instantiations with parameters [12] January 19, 2015
Commented Issue: 12-01-16_1: handling of tuple quantification [10] January 19, 2015

RT @pheras: Leslie Lamport: Thinking for Programmers. On the importance of specifying SW before coding. Intro to TLA+, PlusCal. http://t.co/KpW4wcuBLU

2 months ago
RT @DavidFdzP: I'm looking inside The PlusCal Algorithm Language http://t.co/BZ7aDhX0Ho #springerlink

2 months ago
RT @PaulCichonski: Amazon says they are seeing benefits using TLA+ and pluscal to find bugs in AWS distributed systems. Looks promising http://t.co/IZSx9ruqpt

2 months ago
RT @neil_conway: Verifiable Go looks cool: a subset of Go with temporal logic assertions that can be verified via model checking. http://t.co/HyXuM73HdB

2 months ago
RT @PrologInfo: "Temporal logic and functional reactive programming" (slides, Sergei Winitzki, 2014) http://t.co/VcMqNYrRmf

2 months ago