How can I infer inputs to a function, given an output?
In the worst case, this is impossible.  However, there are techniques for inversion that can work on some programs.  Of course, you shouldn't expect them to work on all programs given that the problem is hard.

Here are a few standard approaches:


Theorem proving. Use the VCGen part of a theorem prover to generate a precondition formula, where if the formula is true, that implies that the function produces the desired output (or divides by zero, etc.).  Then, use an automated solver to try to find a satisfying assignment to that formula.
Symbolic execution. Execute the function symbolically, and build up a symbolic expression that represents the output of the function, in terms of a bunch of variables (unknowns) that represent the inputs to the function.  Then build a formula by setting that expression equal to the desired output, feed that formula to a SMT solver and ask the solver to find a satisfying assignment for the formula.
Concolic execution.  Pick concrete values for the inputs to the function.  Execute the function on those inputs and record what path it took.  On the side, build up a symbolic expression that represents the output of the function, if it follows the same path.  Build up a "path constraint", which is a formula that is the conjunction of all of the branch conditions followed: the path constraint is a formula over symbolic variables representing the inputs, where inputs that make the path constraint true will cause the function to execute the same path that was previously recorded.  Then, write down a formula that represents the statement "the function takes that path, and its output is equal to the desired value", and feed this to a SMT solver or SAT solver and ask it to find a satisfying assignment.  See concolic testing.


These approaches have different tradeoffs and perform differently, but as you can see, they are similar conceptually.  Here are some significant differences:


Theorem proving and symbolic execution can have problems with loops.  For instance, theorem provers usually require you to supply a loop invariant for every loop.  Concolic execution circumvents this by not trying to reason about all possible paths; only a single one.
Theorem proving and symbolic execution can have problems with state space explosion, as the number of possible paths through the function can be exponentially (or even infinitely) large.  Concolic execution circumvents this by not trying to reason about all possible paths; only a single one.
Theorem proving can use more expressive logics, such as fist-order logic.  Symbolic execution and concolic execution often use propositional logic or a SMT extension.


You can find lots of reference material on these approaches.  For instance, today they're taught in a number of advanced (e.g., graduate) program analysis courses, and there are many publications in the research literature on these topics.