• Why3

  • Referenced in 136 articles [sw04438]
  • discharge verification conditions. Why3 comes with a standard library of logical theories (integer and real...
  • CondLean

  • Referenced in 9 articles [sw09986]
  • CondLean 3.0: Improving CondLean for stronger conditional logics. In this paper we present CondLean ... theorem prover for propositional conditional logics...
  • Tweety

  • Referenced in 9 articles [sw22090]
  • knowledge representation formalisms such as classical logics, conditional logics, probabilistic logics, and argumentation. Furthermore, Tweety...
  • Mathpert

  • Referenced in 18 articles [sw24047]
  • found when computational “operators” have logical side conditions that must be satisfied before they...
  • NESCOND

  • Referenced in 5 articles [sw10041]
  • implementation of nested sequent calculi for conditional logics. We present NESCOND, a theorem prover ... normal conditional logics. NESCOND implements some recently introduced NESted sequent calculi for propositional CONDitional logics...
  • StateFlow

  • Referenced in 46 articles [sw04350]
  • modeling and simulating combinatorial and sequential decision logic based on state machines and flow charts ... time-based conditions, and external input signals. With Stateflow you can design logic for supervisory...
  • Kiva-2

  • Referenced in 68 articles [sw08987]
  • conditions and mesh generation have been written for internal combustion engine calculations, the logic...
  • HOL-Boogie

  • Referenced in 14 articles [sw00409]
  • Boogie is a program verification condition generator for an imperative core language. It has front ... annotations in first-order logic.\parIts verification conditions -- constructed via a wp calculus from these...
  • Viper

  • Referenced in 12 articles [sw15038]
  • verification techniques based on first-order logic specifications has benefitted greatly from verification infrastructures such ... back-end tools: in particular, verification condition generators. However, these infrastructures are not well suited ... verification techniques based on separation logic and other permission logics, because they do not provide ... tools for these logics often favour symbolic execution over verification condition generation. Consequently, tool support...
  • AxiomCalc

  • Referenced in 7 articles [sw20253]
  • guarantee standard completeness for the formalized logics. These conditions are implemented in the PROLOG system ... suitable axiomatic extension of Monoidal T-norm Logic MTL and outputs a hypersequent calculus...
  • Mjollnir

  • Referenced in 14 articles [sw38338]
  • applied to any logic that fulfills certain conditions; we illustrate it for linear real arithmetic...
  • iJulienne

  • Referenced in 6 articles [sw09903]
  • present iJulienne, a trace analyzer for conditional rewriting logic theories that can be used...
  • ESBMC

  • Referenced in 8 articles [sw09946]
  • addition, ESBMC can output verification conditions using the SMT logics QF_AUFBV and QF_AUFLIRA...
  • TRP++

  • Referenced in 18 articles [sw14679]
  • Logic based on the temporal resolution calculus. It is released under the terms and conditions ... clausal resolution approach to propositional temporal logic; Creating an experimental environment to try different modifications...
  • MleanCoP

  • Referenced in 8 articles [sw21522]
  • varying domain conditions. The most recent version also supports heterogeneous multimodal logics and outputs...
  • SOLA-VOF

  • Referenced in 44 articles [sw24125]
  • easy-to-use program. Its logical parts are isolated in separate subroutines, and numerous special ... output capabilities, a variety of optional boundary conditions, and instructive internal documentation...
  • VINTE

  • Referenced in 1 article [sw22814]
  • present VINTE, a theorem prover for conditional logics for counterfactual reasoning introduced by Lewis...
  • CFML

  • Referenced in 8 articles [sw13287]
  • tool generates a logical formula that implies any valid post-condition for that program ... they are expressible in standard higher-order logic, allowing to exploit them in practice...
  • Aglet

  • Referenced in 4 articles [sw13305]
  • syntax and proofs of an authorization logic, Garg and Pfenning’s BL$_{0}$, using dependent ... post-conditions drawn from the authorization logic, which permits ephemeral policies that change during execution...
  • LLFp

  • Referenced in 4 articles [sw20866]
  • LLFp: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads ... constructive dependent type theory of the Logical Framework 𝖫𝖥 with monadic, dependent type constructors indexed...