• Smallfoot

  • Referenced in 52 articles [sw09787]
  • Smallfoot: Modular automatic assertion checking with separation logic. Separation logic is a program logic ... tool for checking certain lightweight separation logic specifications. The assertions describe the shapes of data...
  • CiaoPP

  • Referenced in 41 articles [sw12089]
  • call system library predicates and also checking the assertions present in the program ... time tests for assertions which cannot be checked completely at compile-time, etc. The abstract...
  • Toolchain

  • Referenced in 25 articles [sw09517]
  • software toolchain includes static analyzers to check assertions about your program; optimizing compilers to translate ... Toolchain project assures with machine-checked proofs that the assertions claimed...
  • Java PathFinder

  • Referenced in 120 articles [sw07658]
  • model checked using SPIN. The JAVA program may contain assertions, which are translated into similar...
  • SATORI

  • Referenced in 10 articles [sw09597]
  • benchmark circuitsfor an application to assertion checking...
  • Jass

  • Referenced in 11 articles [sw32265]
  • Jass - java with assertions. Design by Contract, proposed by Meyer for the programming language Eiffel ... checks of specification violation and their treatment during program execution. Jass, Java with assertions ... programs with specifications in the form of assertions. The Jass tool is a pre-compiler ... supports refinement, i.e. subtyping,checks and the novel concept oftrace assertions. Trace assertions are used...
  • ABETS

  • Referenced in 3 articles [sw31985]
  • removed. In addition, ABETS employs runtime assertion checking to automate the identification of bugs...
  • 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...
  • Omnibus

  • Referenced in 3 articles [sw04600]
  • support is provided for run-time assertion checking, extended static checking and full formal verification...
  • checkmate

  • Referenced in 4 articles [sw26785]
  • checkmate: Fast and Versatile Argument Checks. Tests and assertions to perform frequent argument checks...
  • Cascade

  • Referenced in 2 articles [sw34344]
  • file specifies one or more assertions to be checked together with restrictions on program behaviors ... generates verification conditions for the specified assertions and checks them using an SMT solver which ... gives a concrete trace showing how an assertion can fail. Version 2.0 supports the majority...
  • ESBMC

  • Referenced in 7 articles [sw09946]
  • state additional properties using assert-statements, that are then checked as well. It also provides...
  • assertive

  • Referenced in 2 articles [sw26787]
  • package assertive: Readable Check Functions to Ensure Code Integrity. Lots of predicates (is_* functions ... check the state of your variables, and assertions (assert_* functions) to throw errors if they...
  • Daikon

  • Referenced in 43 articles [sw04319]
  • program; these are often used in assert statements, documentation, and formal specifications. Examples include being ... many more. Users can extend Daikon to check for additional invariants. Dynamic invariant detection runs...
  • Jacco

  • Referenced in 1 article [sw29268]
  • Jacco is a toolset for model checking of Java actor programs. Jacco currently supports actor ... performs analysis against safety properties (assertion-based model checking). In order to perform model checking...
  • Sather

  • Referenced in 8 articles [sw34049]
  • object-oriented language with garbage collection, statically-checked strong typing, multiple inheritance, separate implementations ... higher-order routines and iterators, exception handling, assertions, preconditions, postconditions, and class invariants. Code...
  • GRASShopper

  • Referenced in 6 articles [sw23304]
  • expressed in a decidable specification logic to check functional correctness properties. The logic supports mixing ... separation logic and first-order logic assertions, yielding expressive yet concise specifications. The input language...
  • FocusCheck

  • Referenced in 3 articles [sw01298]
  • FocusCheck model-checking tool for the verification and easy debugging of assertion violations in sequential ... thereby enhancing usability and readability of model-checking results...
  • CIVL

  • Referenced in 2 articles [sw34345]
  • check a number of properties, including the absence of deadlocks, race conditions, assertion violations, illegal ... bound array indexing; it can also check that two programs are functionally equivalent...
  • SMACK

  • Referenced in 8 articles [sw23311]
  • input programs. In its default mode, assertions are verified up to a given bound ... implementation of algorithms for verification, model checking, and abstract interpretation...