• Sledgehammer

  • Referenced in 124 articles [sw07047]
  • theorem provers (ATPs) to discharge interactive proof obligations arising in Isabelle/HOL. We extended it with...
  • KRAKATOA

  • Referenced in 86 articles [sw03159]
  • components: the WHY tool, which computes proof obligations for a core imperative language annotated with...
  • GF

  • Referenced in 32 articles [sw13667]
  • conditions, such as well-typedness and proof obligations. Multilingual grammars, where one abstract syntax...
  • PIPER

  • Referenced in 28 articles [sw11478]
  • model checking problem, and emit model checking obligations that are discharged using the SPIN model...
  • HIP

  • Referenced in 27 articles [sw09786]
  • construct a set of separation logic proof obligations in the form of formula implications which...
  • MAYA

  • Referenced in 26 articles [sw03423]
  • provers to deal with the actual proof obligations arising from the specification, i.e. to perform...
  • GasLib

  • Referenced in 25 articles [sw17977]
  • transmission network operators. They are obliged to offer as much freely allocable capacity as possible...
  • csp2B

  • Referenced in 21 articles [sw07703]
  • they may be animated and appropriate proof obligations may be generated. Use of csp2B means...
  • HOL-Z

  • Referenced in 11 articles [sw02996]
  • conjectures stated in the specfication, - generating proof obligations concerning the consistency of state and operation ... well as their proof, and - generating proof obligations resulting from refinement statements for functional...
  • SCC

  • Referenced in 11 articles [sw09809]
  • analyzer that generates a set of proof obligations which if discharged, ensures sufficient completeness ... automatically discharge those proof obligations...
  • Isabelle/UTP

  • Referenced in 11 articles [sw21184]
  • that subsumes the need for typing proof obligations in the object-language. Thirdly, proof tactics...
  • GP-COACH

  • Referenced in 10 articles [sw09137]
  • diversity of the population and this obliges the rules to compete and cooperate among themselves...
  • JACK

  • Referenced in 7 articles [sw07878]
  • allows to inspect the generated proof obligations in a Java syntax, and to trace them...
  • MFE

  • Referenced in 4 articles [sw09764]
  • tools can interoperate to discharge proof obligations of different nature without switching between different tool ... mechanism to keep track of pending proof obligations, and allows the execution of several instances...
  • IsaFoR

  • Referenced in 5 articles [sw10106]
  • formal reduction of the proof obligation produced by Isabelle/HOL to the termination of the corresponding...
  • BWare

  • Referenced in 5 articles [sw10405]
  • support the automated verification of proof obligations coming from the development of industrial applications using...
  • NOXclass

  • Referenced in 3 articles [sw35408]
  • resulting in NOXclass, a classifier for distinguishing obligate, non-obligate and crystal packing interactions...
  • RDL

  • Referenced in 4 articles [sw26677]
  • only a tiny portion of the proof obligations arising in many practical verification efforts falls...
  • AODV

  • Referenced in 4 articles [sw29232]
  • that Isabelle/HOL can re-establish most proof obligations automatically and identify exactly the steps that...
  • InvA

  • Referenced in 2 articles [sw10124]
  • degree of automation, verifying automatically many proof obligations. Maude inductive theorem prover ... used to discharge the remaining obligations which are not automatically verified by InvA. Verification...