• MSVL

  • Referenced in 6 articles [sw31710]
  • MSVL: a typed language for temporal logic programming. The development of types is an important ... types in the temporal logic programming language MSVL, which is an executable subset of projection...
  • UMC4M

  • Referenced in 1 article [sw31709]
  • Translating Xd-C programs to MSVL programs. C language is one of the most popular ... based on Modeling, Simulation and Verification Language (MSVL) and its compiler MC is employed ... translated to an MSVL program M and the negation of a desired property ... also translated to an MSVL program M’, then ”M and M” is compiled and executed...
  • C2M

  • Referenced in 1 article [sw31711]
  • Translating Xd-C programs to MSVL programs. C language is one of the most popular ... based on Modeling, Simulation and Verification Language (MSVL) and its compiler MC is employed ... translated to an MSVL program M and the negation of a desired property ... also translated to an MSVL program M’, then “M and M’” is compiled and executed...
  • MSV

  • Referenced in 1 article [sw19203]
  • Modeling, Simulation and Verification Language (MSVL) as the formal language to model and verify...
  • Coq

  • Referenced in 1888 articles [sw00161]
  • Coq is a formal proof management system. It...
  • CUTE

  • Referenced in 65 articles [sw00177]
  • CUTE: a concolic unit testing engine for C...
  • Workcraft

  • Referenced in 6 articles [sw01021]
  • Reliable high-level modeling constructs are crucial to...
  • mCRL2

  • Referenced in 55 articles [sw01496]
  • mCRL2 stands for micro Common Representation Language 2...
  • MuTACLP

  • Referenced in 4 articles [sw01597]
  • MuTACLP: A language for declarative GIS analysis. This...
  • BLAST

  • Referenced in 129 articles [sw02937]
  • BLAST (Berkeley Lazy Abstraction Software verification Tool) is...
  • SLAM

  • Referenced in 153 articles [sw03136]
  • SLAM is a project for checking that software...
  • TINA

  • Referenced in 45 articles [sw03280]
  • The tool TINA -- construction of abstract state spaces...
  • SPIN

  • Referenced in 723 articles [sw03455]
  • Spin is a popular open-source software tool...
  • SMT-LIB

  • Referenced in 196 articles [sw04103]
  • SMT-LIB was created with the expectation that...
  • NuSMV

  • Referenced in 309 articles [sw04131]
  • NuSMV is a symbolic model checker developed as...
  • LLVM

  • Referenced in 89 articles [sw04892]
  • The LLVM Project is a collection of modular...
  • METATEM

  • Referenced in 55 articles [sw06568]
  • MetateM: An introduction. A methodology for the use...
  • DART

  • Referenced in 74 articles [sw07260]
  • DART: directed automated random testing. We present a...
  • CPAchecker

  • Referenced in 54 articles [sw07408]
  • Cpachecker with sequential combination of explicit-state analysis...
  • VeriFast

  • Referenced in 64 articles [sw07705]
  • The VeriFast program verifier. This note describes a...