TLA+ | The way to specify

The TLA+ and PlusCal Resource

Skip to content

Search for:

Java overflow when using RandomSubset to check inductive invariance September 14, 2020
Proving Prefix Safety Properties September 13, 2020
Using formal methods to reason about probabilistic systems September 11, 2020
Artificial coupling of variables September 6, 2020
Postdoc position on Formal Methods and Testing @ TU Graz, Austria September 3, 2020

The (minimal) module end marker is "====". September 22, 2020 lemmy
Break non-determinism in simulation mode by picking one successor state September 21, 2020 lemmy
Break non-determinism in simulation mode by picking one successor state September 21, 2020 lemmy
Un-finalize SubsetValue#elements to implement the FiniteSetsExt!kSubset September 18, 2020 lemmy
Report coverage for state and action constraints. September 17, 2020 lemmy

RT @lemmster: Help me settle a dispute. TLA+ (#tlaplus) is:

6 days ago
RT @TheOfficialACM: At 18:30 CEST on Monday, September 21, #ACMTuringAward recipients Antony Hoare and Leslie Lamport will have a dialo… https://t.co/oFglhCnqGV

2 weeks ago
RT @lemmster: TLA+ Community Event 2020 schedule is out: https://t.co/0a0Nzn9HG4 #tlaplus #pluscal

3 weeks ago
More examples needed! https://t.co/x0dH7u0759

3 weeks ago
RT @lemmster: Thanks for all the great proposals. This will be an awesome #tlaplus community event.

4 weeks ago