The released code of ReluVal in USENIX Security 2018
Switch branches/tags
Nothing to show
Clone or download
Failed to load latest commit information.
nnet restructure Jul 23, 2018
scripts properties Jul 23, 2018
LICENSE license Jul 24, 2018 Neurify updates Oct 7, 2018
interval.h license Jul 24, 2018
makefile restructure Jul 23, 2018
matrix.c license Jul 24, 2018
matrix.h license Jul 24, 2018
network_test.c license Jul 24, 2018
nnet.c Neurify updates Oct 7, 2018
properties license Jul 24, 2018
split.c Neurify updates Oct 7, 2018
split.h license Jul 24, 2018

ReluVal(Usenix Security'18)

ReluVal is a system for formally analyzing self-defined properties on given neural networks by leveraging symbolic interval analysis and iterative refinement.

You can find detailed description of ReluVal in paper Formal Security Analysis of Neural Networks using Symbolic Intervals.

This repository contains the implementation of ReluVal and the evalutions on ACAS Xu described in the paper.

Currently, we have proposed a followup improved system, namely Neurify, proposed in our NIPS 2018 paper Efficient Formal Safety Analysis of Neural Networks. Part of improvements of Neurify have been merged into this repo and successfully improve on average 20 times performance on ACAS Xu dataset compared to ReluVal and achieve on average 5000 times better performance compared to Reluplex. Neurify also supports convolutional models and malware detection models. One can find the implementations of Neurify from Neurify's repo.


OpenBLAS Installation

OpenBLAS library is used for matrix multiplication speedup. So please make sure you have successfully installed OpenBLAS. You can follow following commands to install openblas or find the quick installation guide at OpenBLAS's Installation Guide.

tar -xzf SOpenBLAS-0.2.20.tar.gz
cd OpenBLAS-0.2.20
make PREFIX=/path/to/your/installation install


git clone


Please make sure the path of OpenBLAS is the same as the one in MakeFile. Then you can compile ReluVal with following command:

cd ReluVal

File Structure

  • network_test.c: main file to run with
  • nnet.c: deal with network instance and do symbolic interval analysis
  • split.c: manage iterative refinement and dynamic thread rebalancing
  • matrix.c: matrix operations supported by OpenBLAS
  • nnet/: ACAS Xu models
  • scripts/: scripts to run the ACAS Xu evaluations reported in paper


The main function is in network_test.c. To run the function, you can call the binary ./network_test. It expects at least three arguments. Here is the argument list:

property: the saftety property want to verify

network: the network want to test with

target: wanted label of the property

need to print = 0: whether need to print the detailed information of each split. 0 is not and 1 is yes. Default value is 0.

test for one run = 0: whether need to estimate the output range without split refinement. 0 is no, 1 is yes. Default value is 0.

check mode = 0: choose the mode of formal anlysis. Normal split and check mode is 0. Check adv mode is 1. Check adv mode will prevent further splits as long as the bisection depth goes upper than 20 so as to locate concrete adversarial examples faster. Default value is 0.

The program will terminate in two ways: (1) a concrete adversarial is found, and (2) the property is verified as safe.


Here is an example for running ReluVal:

./network_test 5 ./nnet/ACASXU_run2a_1_1_batch_2000.nnet 4


The ACAS Xu properties reported in the paper are defined in the Appendix A and in the file "properties". One can easily create own properties with following three steps: (1) creating new models in the same style as ones in folder "nnet", (2) adding new bounded input ranges in function load_inputs in file "nnet.c", and (3) adding check function of the property in function check_functions and check_functions1 in file "split.c".

ACAS Xu experiments

The test on ACAS Xu can be easily ran with pre-written scripts in folder "scripts". Here is an example:


Citing ReluVal

@inproceedings {shiqi2018reluval,
	author = {Shiqi Wang and Kexin Pei and Justin Whitehouse and Junfeng Yang and Suman Jana},
	title = {Formal Security Analysis of Neural Networks using Symbolic Intervals},
	booktitle = {27th {USENIX} Security Symposium ({USENIX} Security 18)},
	year = {2018},
	address = {Baltimore, MD},
	url = {},
	publisher = {{USENIX} Association},



Copyright (C) 2018-2019 by its authors and contributors and their institutional affiliations under the terms of modified BSD license.

Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License.