David Shriver

Good question. Unfortunately, DNNV only supports linear constraints in property specifications, so L2 norms cannot be exactly specified. L1 norms should be supported, however. An example of what you have...

Would you also add/edit your description of the pull request please, so that we can keep documentation on the changes that this should be making.

Sorry for the late reply, my life is a bit busy right now. Thanks for another interesting bug. I'm not quite sure where the issue is yet, but my guess...

Great question. Honestly, I don't remember. It looks like that simplification is applied to MaxPool operations that occur either before OR after ReLU operations. I assume I made some assumption...

The submission for DNNF: ``` TOOL_NAME=DNNF REPO=https://github.com/dlshriver/DNNF.git COMMIT=e2dafcc0017bdd555a777e8f6ae96d0af5813bfb SCRIPTS_DIR=scripts/vnncomp ``` The README for the tool submission is here: https://github.com/dlshriver/DNNF/blob/e2dafcc0017bdd555a777e8f6ae96d0af5813bfb/scripts/vnncomp/README.md

For DNNF, our `install_tool.sh` script should take care of creating a python virtual environment and installing the required frameworks, and the other scripts should automatically activate this virtual environment, so...

*"Correct violated (where random tests or simple adversarial example generation did not succeed)"* seems to have been removed, but *"Correct violated (where random tests or simple adversarial example generation succeeded)"*...

I think it might be worth having separate scores for "violated" and "holds" problems in addition to a combined score where the results are weighted equally, similar to SMT-COMP which...

I disagree with @mnmueller that finding a counterexample is easier than certifying the absence of one. Certainly for some problems it can be easy to find a counterexample, just as...

Very interesting. I've confirmed this results in that error, but I don't have a solution yet. It still passes the test suite so it does work on some simple problems....