i've used drmaciver's property testing library hypothesis to find bugs in c libraries before; it has shrinking. 'doesn't crash' is the easiest property to define, but a bit fiddly to connect to property testing libraries, because you have to spawn a subprocess. in one case i just used fork, _exit, and wait, but in some cases things get ugly then (posix threads guarantee you almost nothing, but fortunately i wasn't using threads)
his 'minithesis' is the best way i've found to learn about implementing property-based testing
sat and smt solvers have gotten astoundingly good, and most of the leading ones are free software. smt-comp shows off new gains every year and has a lineup of the leaders
z3 is a particularly easy smt solver to get started with, in part because of its convenient python binding
a thing sat/smt and property-based testing have in common is that they both solve inverse problems, allowing you to program at a more declarative level
his 'minithesis' is the best way i've found to learn about implementing property-based testing
sat and smt solvers have gotten astoundingly good, and most of the leading ones are free software. smt-comp shows off new gains every year and has a lineup of the leaders
z3 is a particularly easy smt solver to get started with, in part because of its convenient python binding
a thing sat/smt and property-based testing have in common is that they both solve inverse problems, allowing you to program at a more declarative level