• TLA

  • Referenced in 26 articles [sw04442]
  • TLA stands for the Temporal Logic of Actions, but it has become a shorthand ... referring to 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 ... needed to write simple mathematics precisely. TLA+ is especially well suited for writing high-level...
  • TLC

  • Referenced in 12 articles [sw09530]
  • model checker for specifications written in TLA+. TLA+ is a specification language based ... TLA, the Temporal Logic of Actions. See the TLA web page for general information about ... TLA. You will most likely want to use TLC from the TLA Toolbox. Downloading ... latest version of all the TLA+ tools, including TLC. How to write TLA+ specifications...
  • TLAPS

  • Referenced in 9 articles [sw09528]
  • TLA+ Proof System (TLAPS) mechanically checks TLA+ proofs. TLA+ is a general-purpose formal specification ... describing concurrent and distributed systems. The TLA+ proof language is declarative, hierarchical, and scalable ... does not handle some features of TLA+. See the list of currently unsupported TLA+ features ... extension to the full TLA+ language is under active development. However, TLAPS is now suitable...
  • PlusCal

  • Referenced in 8 articles [sw09529]
  • concurrent algorithms. It is based on the TLA + specification language, and a PlusCal algorithm ... automatically translated to a TLA + specification that can be checked with the TLC model checker...
  • DiskPaxos

  • Referenced in 2 articles [sw29236]
  • practical tool for verifying properties of TLA+ specifications...
  • Dixit

  • Referenced in 1 article [sw10564]
  • proving correctness of the abstraction w.r.t. TLA+ system specifications can be generated, correctness properties expressed...
  • Maple

  • Referenced in 5124 articles [sw00545]
  • The result of over 30 years of cutting...
  • TulaFale

  • Referenced in 14 articles [sw00986]
  • TulaFale: a security tool for web services. Web...
  • APL

  • Referenced in 76 articles [sw01165]
  • APL (named after the book A Programming Language...
  • Alloy

  • Referenced in 29 articles [sw01247]
  • Alloy: A new technology for software modelling. Alloy...
  • SPIN

  • Referenced in 712 articles [sw03455]
  • Spin is a popular open-source software tool...
  • PVS

  • Referenced in 620 articles [sw03484]
  • PVS is a verification system: that is, a...
  • Haskell

  • Referenced in 851 articles [sw03521]
  • Haskell is a standardized, general-purpose purely functional...
  • LabVIEW

  • Referenced in 55 articles [sw04369]
  • LabVIEW is a highly productive development environment that...
  • Uppaal

  • Referenced in 634 articles [sw04702]
  • Uppaal is an integrated tool environment for modeling...
  • ISP

  • Referenced in 12 articles [sw04895]
  • ISP (”In-situ Partial Order”) is a tool...
  • MPI/MPICH

  • Referenced in 161 articles [sw06126]
  • MPI / MPICH Message Passing Interface MPI is the...
  • Maude

  • Referenced in 666 articles [sw06233]
  • Maude is a high-performance reflective language and...
  • ProB

  • Referenced in 63 articles [sw07084]
  • ProB: an automated analysis toolset for the B...
  • Kodkod

  • Referenced in 24 articles [sw07090]
  • Kodkod: A relational model finder. The key design...