• JPAX

  • Referenced in 30 articles [sw09906]
  • concurrency errors such as deadlocks and data races. The concurrency analysis requires no user provided ... temporal logic verification, the deadlock analysis and the data race analysis. Temporal logic specifications...
  • TyPiCal

  • Referenced in 8 articles [sw23207]
  • analyses or program transformations: lock-freedom analysis, deadlock-freedom analysis, useless-code elimination, information flow ... communication succeeds or not. The lock-freedom analysis can answer, e.g., the following questions about ... interface for TyPiCal’s deadlock-freedom analysis here...
  • RacerX

  • Referenced in 16 articles [sw09941]
  • flow-sensitive, interprocedural analysis to detect both race conditions and deadlocks. It is explicitly designed ... novel techniques to counter the impact of analysis mistakes. The tool is fast, requiring between ... flow-sensitive, interprocedural analysis to detect both race conditions and deadlocks. It uses novel strategies...
  • Gopherlyzer

  • Referenced in 2 articles [sw23206]
  • Gopherlyzer: Static Trace-Based Deadlock Analysis for Synchronous Mini-Go. We consider the problem ... static deadlock detection for programs in the Go programming language which make use of synchronous ... channel communications. In our analysis, regular expressions extended with a fork operator capture the communication ... simple criterion that characterizes traces of deadlock-free programs, we develop automata-based methods...
  • IMITATOR

  • Referenced in 31 articles [sw00439]
  • software tool for parametric verification and robustness analysis of real-time systems with parameters ... robustness, untimed language preservation, non-Zeno or deadlock-free parameter synthesis, accepting cycle synthesis...
  • Timed Rebeca

  • Referenced in 3 articles [sw40758]
  • Timed Rebeca schedulability and deadlock freedom analysis using bounded floating time transition system. Timed Rebeca ... approach for checking schedulability and deadlock freedom of Timed Rebeca models. The key features...
  • CSP

  • Referenced in 1 article [sw08678]
  • synchronizations, many analyses such as deadlock analysis, reliability analysis, and program slicing try to predict...
  • CSPsim

  • Referenced in 4 articles [sw13312]
  • safety and increases deadlocks involving callbacks. par Through the creation and analysis of the model...
  • Autolocker

  • Referenced in 4 articles [sw09532]
  • most burdens of lock-based programming, including deadlocks. Significantly, pessimistic atomic sections separate correctness from ... program analysis to determine a correct locking policy free of deadlocks and race conditions...
  • GKLEE

  • Referenced in 11 articles [sw12794]
  • often contain correctness errors such as races, deadlocks, or may compute the wrong result. Existing ... exploration. Existing tools based on conservative static analysis or conservative modeling of SIMD concurrency generate...
  • Helena

  • Referenced in 11 articles [sw04384]
  • High level Petri nets analysis with Helena. This paper presents the high level Petri nets ... reachable states of the system, and deadlock freeness. Some features of Helena make it particularly...
  • Quasar

  • Referenced in 3 articles [sw01278]
  • analysis of the model both by structural techniques and model-checking techniques; reporting deadlock...
  • MARMOT

  • Referenced in 6 articles [sw09407]
  • MARMOT: an MPI analysis and checking tool. This chapter discusses MARMOT, a tool to check ... occurrence of race conditions or deadlocks. Examples are the introduction of irreproducibility, deadlocks, and incorrect...
  • JaVis

  • Referenced in 4 articles [sw00469]
  • such as tracing, visualization, and automated error analysis. Therefore, we have developed the JaVis environment ... traces. Traces are automatically analyzed for deadlocks. The tracing is implemented using the Java Debug...
  • Alcove

  • Referenced in 4 articles [sw41058]
  • VErifier) is a framework for the automatic analysis of Access Permission based programs. The tool ... relevant properties of the program such us: Deadlocks: the program cannot terminate. Concurrent executions: whether...
  • McPatom

  • Referenced in 2 articles [sw42811]
  • McPatom: A Predictive Analysis Tool for Atomicity Violation Using Model Checking. Multi-thread programs ... large number of interleavings. Most non-deadlock concurrency bugs are atomicity violation bugs...
  • STANSE

  • Referenced in 2 articles [sw26812]
  • finding bugs in C programs using static analysis. Its two main design goals ... automata-based formalism, ThreadChecker detects deadlocks among multiple threads, LockChecker finds locking errors based...
  • ACL2

  • Referenced in 291 articles [sw00060]
  • ACL2 is both a programming language in which...
  • Dafny

  • Referenced in 74 articles [sw00183]
  • Dafny is an imperative object-based language with...
  • D-Finder

  • Referenced in 17 articles [sw00200]
  • D-Finder tool implements a compositional method for...