
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 welltypedness 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...

HOLZ
 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 objectlanguage. Thirdly, proof tactics...

GPCOACH
 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, nonobligate 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 reestablish 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...