• J-LO

  • Referenced in 3 articles [sw32260]
  • Logical Observer. A tool for runtime-checking temporal assertions. J-LO, the Java Logical Observer ... tool for runtime-checking temporal assertions in Java 5 applications. Temporal properties (see below ... instruments the application with the appropriate runtime checks...
  • ABETS

  • Referenced in 3 articles [sw31985]
  • removed. In addition, ABETS employs runtime assertion checking to automate the identification of bugs...
  • JBMC

  • Referenced in 2 articles [sw25908]
  • Java programs. It checks runtime exceptions and user-definded assertions. The verification is performed...
  • Praspel

  • Referenced in 1 article [sw30376]
  • runtime assertion checker, which decides whether a test passes or fails by checking the satisfaction...
  • JayHorn

  • Referenced in 2 articles [sw25903]
  • JayHorn is a software model checking tool for Java. JayHorn tries to find a proof ... states are specified by adding runtime assertions (where some assertions may be generated, e.g., that...
  • TXP

  • Referenced in 1 article [sw32264]
  • Dynamic Assertions Using TXP. In this paper, we present a new temporal property specification language ... simulation runtime, as well as to provide the input specification for formal property checking ... inadequate for concise specification of complex assertions where logic relationships involve multi cycle behavior ... complex assertions. A TXP engine has been developed to monitor the properties at runtime...
  • 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...
  • QEPCAD

  • Referenced in 283 articles [sw00752]
  • QEPCAD B: A program for computing with semi...
  • ML

  • Referenced in 522 articles [sw01218]
  • ML (’Meta Language’) is a general-purpose functional...
  • jContractor

  • Referenced in 10 articles [sw01488]
  • jContractor: Introducing design-by-contract to Java using...
  • veriSoft

  • Referenced in 92 articles [sw01489]
  • VeriSoft automatically searches for coordination problems (deadlocks, etc...
  • FoCs

  • Referenced in 20 articles [sw01591]
  • FoCs -- automatic generation of simulation checkers from formal...
  • Ada95

  • Referenced in 293 articles [sw01753]
  • Ada is a structured, statically typed, imperative, wide...
  • LARCH

  • Referenced in 104 articles [sw02126]
  • The Larch family of languages supports a two...
  • SPARK

  • Referenced in 48 articles [sw03124]
  • Using the SPARK toolset for showing the absence...
  • SLAM

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

  • Referenced in 89 articles [sw03159]
  • The KRAKATOA tool for certification of JAVA/JAVACARD programs...
  • SPIN

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