• F*

  • Referenced in 20 articles [sw27563]
  • monadic effects, refinement types, and a weakest precondition calculus. Together, these features allow expressing precise...
  • ZRC

  • Referenced in 14 articles [sw21827]
  • this language. Moreover, we present the weakest precondition semantics of ZRC-L, which...
  • pGCL

  • Referenced in 12 articles [sw13078]
  • both), using either Hoare triples, or weakest-precondition entailment, in the style of GCL. This...
  • TRACER

  • Referenced in 12 articles [sw09484]
  • unbounded loops. TRACER computes interpolants (using weakest preconditions among other methods) from infeasible paths...
  • Snugglebug

  • Referenced in 7 articles [sw13707]
  • Snugglebug: a powerful approach to weakest preconditions. Symbolic analysis shows promise as a foundation ... based on interprocedural backwards propagation of weakest preconditions. We present several novel techniques to improve ... inexpensive, custom logic simplifier with weakest precondition computation dramatically improves performance. We have implemented...
  • Algebraic_VCs

  • Referenced in 2 articles [sw32217]
  • algebra with tests, verification components for weakest preconditions and strongest postconditions based on Kleene algebra ... program trace semantics into the weakest precondition component...
  • RBAC-PAT

  • Referenced in 3 articles [sw00782]
  • various properties including reachability, availability, containment, weakest precondition, dead roles, and information flows...
  • DynAlloy

  • Referenced in 3 articles [sw39829]
  • adaptation of Dijkstra’s weakest liberal precondition. These assertions, defined in terms of actions, allow...
  • EIOD

  • Referenced in 1 article [sw10040]
  • suspicious integer overflow vulnerabilities. Finally the weakest preconditions technique is used to validate the suspicious...
  • LCTD

  • Referenced in 1 article [sw17728]
  • method for constructing the weakest precondition based refinement operator employed by {sc Dash} for instructions...
  • Boolector

  • Referenced in 32 articles [sw00085]
  • Boolector: an efficient SMT solver for bit-vectors...
  • Coq

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

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

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

  • Referenced in 6445 articles [sw00554]
  • Almost any workflow involves computing results, and that...
  • MiniSat

  • Referenced in 584 articles [sw00577]
  • An extensible SAT-solver. MiniSat is a minimalistic...
  • Nitpick

  • Referenced in 64 articles [sw00622]
  • Nitpick is a counterexample generator for Isabelle/HOL that...
  • Theorema

  • Referenced in 150 articles [sw00961]
  • The software system Theorema provides a uniform logic...
  • LARCH

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