PKC Workflow/System Verification by TLA+/Context

From PKC
Revision as of 05:47, 30 August 2021 by KevinTung (talk | contribs)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to navigation Jump to search
  1. To analyze a system correctly before it is implemented, a language to model the system and automatic tools to prove the system is required.
  2. TLA+ is a high-level language for modeling programs and systems--especially concurrent and distributed ones.