Crowdsourcing promises to quasi-automate tasks that cannot be
automated otherwise.  Success stories like natural language
translation or recognition of cats in images show that carefully
crafted crowdsourcing tasks solve large problem instances which could
not be solved otherwise. To utilize crowdsourcing, one has to define
the problem in a way that is easy to split into small tasks, that the
tasks are easy to solve for humans and hard to solve for a machine,
and that the machine can efficiently check if the solution is correct.
In this paper we discuss a novel approach of using crowdsourcing to
assist software verification. We argue that Horn clauses form a good
base for crowdsourcing since they are easy to subdivide, and that
logic abduction is a suitable task since it is hard to find abductive
inferences for Horn clauses automatically, but it is easy to check if
an inference makes a Horn clause valid. We describe a prototype
implementation, we show how crowdsourcing integrates in the
verification process, and present preliminary results.