AVR: Abstractly Verifying Reachability
419
7 Conclusions
AVR provides a variety of techniques to efficiently perform automatic word-level
verification using SMT solvers with provable guarantees and security. AVR has
been effective in hardware verification [17,33,34] and shows significant promise
for the verification of distributed protocols [44,45]. In the future, we plan to
address some of its current limitations and extend its application to practical
verification problems beyond the hardware domain.
Data Availability Statement and Acknowledgments. The software and datasets
generated and analyzed during the current study are available in the Zenodo
repository: https://doi.org/10.5281/zenodo.3677545. The authors would like to
thank Ranan Fraer, Ravi Prakash, Habeeb Farah and Ziyad Hanna from Cadence
Design Systems for their help in shaping some of the concepts presented in this
paper.
References
1. Apache HTTP server project. https://httpd.apache.org
2. AVR (github). https://github.com/aman-goel/avr
3. Btor2Tools. https://github.com/Boolector/btor2tools
4. BtorSIM. https://github.com/Boolector/btor2tools/tree/master/src/btorsim
5. Experiments. https://github.com/aman-goel/tacas20ae
6. National Vulnerability Database - CVE-2004-0940. https://nvd.nist.gov/vuln/
detail/CVE-2004-0940
7. National Vulnerability Database - CVE-2006-3747. https://nvd.nist.gov/vuln/
detail/CVE-2006-3747
8. Verification Modulo Theories. http://www.vmt-lib.org
9. Ieee standard for systemverilog–unified hardware design, specification, and verification language. IEEE Std 1800-2017 (Revision of IEEE Std 1800-2012) pp. 1–1315
(Feb 2018). https://doi.org/10.1109/IEEESTD.2018.8299595
10. Andraus, Z.S., Sakallah, K.A.: Automatic abstraction and verification of verilog
models. In: Proceedings. 41st Design Automation Conference, 2004. pp. 218–223
(July 2004). https://doi.org/10.1145/996566.996629
11. Babi´ c, D., Hu, A.J.: Structural abstraction of software verification conditions.
In: Damm, W., Hermanns, H. (eds.) Computer Aided Verification. pp. 366–378.
Springer Berlin Heidelberg, Berlin, Heidelberg (2007)
12. Barrett, C., Deters, M., de Moura, L., Oliveras, A., Stump, A.: 6 years of
SMT-COMP. Journal of Automated Reasoning 50(3), 243–277 (Apr 2012).
https://doi.org/10.1007/s10817-012-9246-5
13. Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library
(SMT-LIB). www.SMT-LIB.org (2016)
14. Berkeley Logic Synthesis and Verification Group: ABC: A system for sequential
synthesis and verification. http://www.eecs.berkeley.edu/ ∼ alanmi/abc/ (2017)
15. Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without bdds.
In: Cleaveland, W.R. (ed.) Tools and Algorithms for the Construction and Analysis
of Systems. pp. 193–207. Springer Berlin Heidelberg, Berlin, Heidelberg (1999)
419
7 Conclusions
AVR provides a variety of techniques to efficiently perform automatic word-level
verification using SMT solvers with provable guarantees and security. AVR has
been effective in hardware verification [17,33,34] and shows significant promise
for the verification of distributed protocols [44,45]. In the future, we plan to
address some of its current limitations and extend its application to practical
verification problems beyond the hardware domain.
Data Availability Statement and Acknowledgments. The software and datasets
generated and analyzed during the current study are available in the Zenodo
repository: https://doi.org/10.5281/zenodo.3677545. The authors would like to
thank Ranan Fraer, Ravi Prakash, Habeeb Farah and Ziyad Hanna from Cadence
Design Systems for their help in shaping some of the concepts presented in this
paper.
References
1. Apache HTTP server project. https://httpd.apache.org
2. AVR (github). https://github.com/aman-goel/avr
3. Btor2Tools. https://github.com/Boolector/btor2tools
4. BtorSIM. https://github.com/Boolector/btor2tools/tree/master/src/btorsim
5. Experiments. https://github.com/aman-goel/tacas20ae
6. National Vulnerability Database - CVE-2004-0940. https://nvd.nist.gov/vuln/
detail/CVE-2004-0940
7. National Vulnerability Database - CVE-2006-3747. https://nvd.nist.gov/vuln/
detail/CVE-2006-3747
8. Verification Modulo Theories. http://www.vmt-lib.org
9. Ieee standard for systemverilog–unified hardware design, specification, and verification language. IEEE Std 1800-2017 (Revision of IEEE Std 1800-2012) pp. 1–1315
(Feb 2018). https://doi.org/10.1109/IEEESTD.2018.8299595
10. Andraus, Z.S., Sakallah, K.A.: Automatic abstraction and verification of verilog
models. In: Proceedings. 41st Design Automation Conference, 2004. pp. 218–223
(July 2004). https://doi.org/10.1145/996566.996629
11. Babi´ c, D., Hu, A.J.: Structural abstraction of software verification conditions.
In: Damm, W., Hermanns, H. (eds.) Computer Aided Verification. pp. 366–378.
Springer Berlin Heidelberg, Berlin, Heidelberg (2007)
12. Barrett, C., Deters, M., de Moura, L., Oliveras, A., Stump, A.: 6 years of
SMT-COMP. Journal of Automated Reasoning 50(3), 243–277 (Apr 2012).
https://doi.org/10.1007/s10817-012-9246-5
13. Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library
(SMT-LIB). www.SMT-LIB.org (2016)
14. Berkeley Logic Synthesis and Verification Group: ABC: A system for sequential
synthesis and verification. http://www.eecs.berkeley.edu/ ∼ alanmi/abc/ (2017)
15. Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without bdds.
In: Cleaveland, W.R. (ed.) Tools and Algorithms for the Construction and Analysis
of Systems. pp. 193–207. Springer Berlin Heidelberg, Berlin, Heidelberg (1999)