User Tools
start
Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
start [2016/07/20 00:28] jonathan [PVS] |
start [2017/08/30 21:50] (current) jonathan |
||
|---|---|---|---|
| Line 9: | Line 9: | ||
| [[http://pvs.eecs.yorku.ca|http://pvs.eecs.yorku.ca]] | [[http://pvs.eecs.yorku.ca|http://pvs.eecs.yorku.ca]] | ||
| + | |||
| + | ====== TLA+ ====== | ||
| + | |||
| + | TLA stands for the Temporal Logic of Actions. TLA+ is the TLA specification language and the PlusCal algorithm language, together with their associated tools. TLA+ is based on the idea that the best way to describe things formally is with simple mathematics, and that a specification language should contain as little as possible beyond what is needed to write simple mathematics precisely. TLA+ is especially well suited for writing high-level specifications of concurrent and distributed systems. | ||
| + | |||
| + | [[http://tla.eecs.yorku.ca|http://tla.eecs.yorku.ca]] | ||
start.1468974500.txt.gz ยท Last modified: 2016/07/20 00:28 by jonathan
Page Tools
