[racket-dev] Announcing Soft Contract Verification tool

From: David Van Horn (dvanhorn at cs.umd.edu)
Date: Thu Jan 15 15:14:26 EST 2015

On 1/15/15, 2:48 PM, Robby Findler wrote:
> Can you randomly make up programs from your grammar, get example 
> errors from the tool, and then run those programs to see if you
> find bugs in the analysis like that one?

Yes, we're planning to do this.

> That said, I don't see how the bug in >=/c is coming in here. Can
> you explain more?

On further inspection, the counterexample is wrong.  (There are
counterexamples due to the model of >=/c, but the one that reported is
not an actual one.)  This will be fixed shortly.

David


Posted on the dev mailing list.