TLA+ | The way to specify

The TLA+ and PlusCal Resource

Skip to content

Search for:

Created Issue: Definition Override Toolbox Wizard Bug [12] March 4, 2015
Source code checked in, #61f059ff79ac47862915b3da90eac7f6468fc358 March 2, 2015
Source code checked in, #1764c791e7b687df539c93f101792a2a7bd622b6 February 27, 2015
Source code checked in, #aa51927ed0e7f086d8a3910bfeba1a1e59ba4049 February 27, 2015
Source code checked in, #8d5f09f01c27560ed8a9dc7f087d94125f347364 February 27, 2015

Edited Unassigned: Obligation unfolding a definition from a module instance captures variables [35] February 25, 2015
Created Unassigned: Obligation unfolding a theorem from a module instance captures variables [35] February 25, 2015
Closed Unassigned: SANY accepts step names in DEF references (15-01-19) [34] February 25, 2015
Commented Unassigned: SANY accepts step names in DEF references (15-01-19) [34] February 5, 2015
Edited Unassigned: SANY accepts step names in DEF references (15-01-19) [34] February 5, 2015

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

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

3 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

3 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

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

3 months ago