• CafeOBJ

  • Referenced in 167 articles [sw06232]
  • verification. We report on a machine supported method for verifying safety properties of dynamic systems...
  • d/dt

  • Referenced in 37 articles [sw10314]
  • systems with linear continuous dynamics with uncertain input. The verification procedure is based...
  • Dafny

  • Referenced in 66 articles [sw00183]
  • static verification of programs. It is imperative, sequential, supports generic classes, dynamic allocation, and inductive ... ghost constructs are used only during verification; the compiler omits them from the executable code.The...
  • KeYmaera

  • Referenced in 41 articles [sw03709]
  • natural specification and verification logic for hybrid systems. KeYmaera supports differential dynamic logic, which ... dynamic logic for hybrid programs, a program notation for hybrid automata. For automating the verification...
  • Theano

  • Referenced in 76 articles [sw05894]
  • stability optimizations, dynamic C code generation, and extensive unit-testing and self-verification. Theano...
  • HSolver

  • Referenced in 42 articles [sw07419]
  • HSolver is a program for verification of hybrid systems based on the constraint solver RSOLVER ... optimized for simpler continuous dynamics...
  • SpaceEx

  • Referenced in 70 articles [sw10939]
  • SpaceEx: Scalable Verification of Hybrid Systems. We present a scalable reachability algorithm for hybrid systems ... with piecewise affine, non-deterministic dynamics. It combines polyhedra and support function representations of continuous ... implemented as part of SpaceEx, a new verification platform for hybrid systems, available at spaceex.imag.fr...
  • CakeML

  • Referenced in 46 articles [sw08799]
  • permitted by the semantics of CakeML. Our verification effort touches on a breadth of topics ... including lexing, parsing, type checking, incremental and dynamic compilation, garbage collection, arbitrary-precision arithmetic ... demonstrating that each piece of such a verification effort can in practice be composed with...
  • HYSDEL

  • Referenced in 38 articles [sw05200]
  • HYSDEL transforms it to the mixed-logical dynamical (MLD) form which can be immediately used ... optimization, to solve, e.g., optimal control, safety verification, or estimation and fault detection problems...
  • DyTa

  • Referenced in 3 articles [sw22848]
  • DyTa: dynamic symbolic execution guided with static verification results. Software-defect detection is an increasingly ... detect defects in a program, static verification and dynamic test generation are two important proposed ... address the limitations of static verification and dynamic test generation, we present an automated defect ... called DyTa, that combines both static verification and dynamic test generation. DyTa consists...
  • CBMC

  • Referenced in 77 articles [sw09719]
  • with other languages, such as Verilog. The verification is performed by unwinding the loops ... aimed for embedded software, it also supports dynamic memory allocation using malloc...
  • KeY

  • Referenced in 63 articles [sw09969]
  • integrate design, implementation, formal specification, and formal verification of object-oriented software as seamlessly ... novel theorem prover for the first-order Dynamic Logic for Java with a user-friendly...
  • JNuke

  • Referenced in 3 articles [sw28382]
  • JNuke: Efficient dynamic analysis for Java. JNuke is a framework for verification and model checking ... example exploration. Efficiency is crucial in dynamic verification. Therefore JNuke has been written from scratch...
  • GROOVE

  • Referenced in 50 articles [sw09480]
  • GRaphs for Object-Oriented VErification (GROOVE). GROOVE is a project centered around ... formal foundation for model transformation and dynamic semantics, and the ability to verify model transformation...
  • C2e2

  • Referenced in 9 articles [sw20139]
  • C2e2: A verification tool for stateflow models. Compare Execute Check Engine (C2E2) is a tool ... system and Stateflow models. It supports nonlinear dynamics...
  • ATGen

  • Referenced in 11 articles [sw07275]
  • symbolic execution The verification and validation of software through dynamic testing is an area...
  • Galileo

  • Referenced in 13 articles [sw00316]
  • around Galileo, an experimental software tool supporting dynamic fault tree analysis and having, as additional ... modeling functions based on mathematical validation and verification...
  • DynaMate

  • Referenced in 2 articles [sw14286]
  • loop invariants for automatic full functional verification. DYNAMATE is a tool that automatically infers loop...
  • COMBINE

  • Referenced in 1 article [sw01423]
  • phases: static verification and dynamic verification. In fact, COMBINE has been developed as a published...
  • Jass

  • Referenced in 11 articles [sw32265]
  • dynamically tested. Besides the standard Design by Contract features known from classical program verification ... Trace assertions are used to monitor the dynamic behaviour of objects in time...