AVR: Abstractly Verifying Reachability
421
33. Goel, A., Sakallah, K.: Empirical evaluation of ic3-based model checking techniques on verilog rtl designs. In: 2019 Design, Automation Test
in Europe Conference Exhibition (DATE). pp. 618–621 (March 2019).
https://doi.org/10.23919/DATE.2019.8715289
34. Goel, A., Sakallah, K.: Model checking of verilog rtl using ic3 with syntax-guided
abstraction. In: Badger, J.M., Rozier, K.Y. (eds.) NASA Formal Methods. pp.
166–185. Springer International Publishing, Cham (2019)
35. Goel, A., Sakallah, K.: AVR: Abstractly Verifying Reachability (Feb 2020).
https://doi.org/10.5281/zenodo.3677545
36. Goldberg, E., G¨ udemann, M., Kroening, D., Mukherjee, R.: Efficient verification
of multi-property designs (the benefit of wrong assumptions). In: 2018 Design,
Automation Test in Europe Conference Exhibition (DATE). pp. 43–48 (March
2018). https://doi.org/10.23919/DATE.2018.8341977
37. Henzinger, T.A., Qadeer, S., Rajamani, S.K.: You assume, we guarantee: Methodology and case studies. In: Hu, A.J., Vardi, M.Y. (eds.) Computer Aided Verification.
pp. 440–451. Springer Berlin Heidelberg, Berlin, Heidelberg (1998)
38. Jefferson, C., Miguel, A., Miguel, I., Tarim, S.A.: Modelling and solving english
peg solitaire. Computers & Operations Research 33(10), 2935–2959 (Oct 2006).
https://doi.org/10.1016/j.cor.2005.01.018
39. Kotovsky, K., Hayes, J., Simon, H.: Why are some problems hard? evidence from tower of hanoi. Cognitive Psychology 17(2), 248–294 (Apr 1985).
https://doi.org/10.1016/0010-0285(85)90009-x
40. Ku, K., Hart, T.E., Chechik, M., Lie, D.: A buffer overflow benchmark for
software model checkers. In: Proceedings of the Twenty-Second IEEE/ACM
International Conference on Automated Software Engineering. p. 389–392.
ASE ’07, Association for Computing Machinery, New York, NY, USA (2007).
https://doi.org/10.1145/1321631.1321691
41. Lee, S., Sakallah, K.A.: Unbounded scalable verification based on approximate
property-directed reachability and datapath abstraction. In: Biere, A., Bloem, R.
(eds.) Computer Aided Verification. pp. 849–865. Springer International Publishing, Cham (2014)
42. Liffiton, M.H., Sakallah, K.A.: Algorithms for computing minimal unsatisfiable
subsets of constraints. Journal of Automated Reasoning 40(1), 1–33 (Sep 2007).
https://doi.org/10.1007/s10817-007-9084-z
43. Lowe, G.: An attack on the needham-schroeder public-key authentication protocol. Information Processing Letters 56(3), 131 – 133 (1995).
https://doi.org/10.1016/0020-0190(95)00144-2
44. Ma, H., Goel, A., Jeannin, J.B., Kapritsos, M., Kasikci, B., Sakallah, K.A.: I4: Incremental inference of inductive invariants for verification of distributed protocols.
In: Proceedings of the 27th ACM Symposium on Operating Systems Principles. p.
370–384. SOSP ’19, Association for Computing Machinery, New York, NY, USA
(2019). https://doi.org/10.1145/3341301.3359651
45. Ma, H., Goel, A., Jeannin, J.B., Kapritsos, M., Kasikci, B., Sakallah, K.A.: Towards
automatic inference of inductive invariants. In: Proceedings of the Workshop on
Hot Topics in Operating Systems. p. 30–36. HotOS ’19, Association for Computing
Machinery, New York, NY, USA (2019). https://doi.org/10.1145/3317550.3321451
46. McMillan, K.L.: Applications of craig interpolants in model checking. In: Halbwachs, N., Zuck, L.D. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 1–12. Springer Berlin Heidelberg, Berlin, Heidelberg (2005)
421
33. Goel, A., Sakallah, K.: Empirical evaluation of ic3-based model checking techniques on verilog rtl designs. In: 2019 Design, Automation Test
in Europe Conference Exhibition (DATE). pp. 618–621 (March 2019).
https://doi.org/10.23919/DATE.2019.8715289
34. Goel, A., Sakallah, K.: Model checking of verilog rtl using ic3 with syntax-guided
abstraction. In: Badger, J.M., Rozier, K.Y. (eds.) NASA Formal Methods. pp.
166–185. Springer International Publishing, Cham (2019)
35. Goel, A., Sakallah, K.: AVR: Abstractly Verifying Reachability (Feb 2020).
https://doi.org/10.5281/zenodo.3677545
36. Goldberg, E., G¨ udemann, M., Kroening, D., Mukherjee, R.: Efficient verification
of multi-property designs (the benefit of wrong assumptions). In: 2018 Design,
Automation Test in Europe Conference Exhibition (DATE). pp. 43–48 (March
2018). https://doi.org/10.23919/DATE.2018.8341977
37. Henzinger, T.A., Qadeer, S., Rajamani, S.K.: You assume, we guarantee: Methodology and case studies. In: Hu, A.J., Vardi, M.Y. (eds.) Computer Aided Verification.
pp. 440–451. Springer Berlin Heidelberg, Berlin, Heidelberg (1998)
38. Jefferson, C., Miguel, A., Miguel, I., Tarim, S.A.: Modelling and solving english
peg solitaire. Computers & Operations Research 33(10), 2935–2959 (Oct 2006).
https://doi.org/10.1016/j.cor.2005.01.018
39. Kotovsky, K., Hayes, J., Simon, H.: Why are some problems hard? evidence from tower of hanoi. Cognitive Psychology 17(2), 248–294 (Apr 1985).
https://doi.org/10.1016/0010-0285(85)90009-x
40. Ku, K., Hart, T.E., Chechik, M., Lie, D.: A buffer overflow benchmark for
software model checkers. In: Proceedings of the Twenty-Second IEEE/ACM
International Conference on Automated Software Engineering. p. 389–392.
ASE ’07, Association for Computing Machinery, New York, NY, USA (2007).
https://doi.org/10.1145/1321631.1321691
41. Lee, S., Sakallah, K.A.: Unbounded scalable verification based on approximate
property-directed reachability and datapath abstraction. In: Biere, A., Bloem, R.
(eds.) Computer Aided Verification. pp. 849–865. Springer International Publishing, Cham (2014)
42. Liffiton, M.H., Sakallah, K.A.: Algorithms for computing minimal unsatisfiable
subsets of constraints. Journal of Automated Reasoning 40(1), 1–33 (Sep 2007).
https://doi.org/10.1007/s10817-007-9084-z
43. Lowe, G.: An attack on the needham-schroeder public-key authentication protocol. Information Processing Letters 56(3), 131 – 133 (1995).
https://doi.org/10.1016/0020-0190(95)00144-2
44. Ma, H., Goel, A., Jeannin, J.B., Kapritsos, M., Kasikci, B., Sakallah, K.A.: I4: Incremental inference of inductive invariants for verification of distributed protocols.
In: Proceedings of the 27th ACM Symposium on Operating Systems Principles. p.
370–384. SOSP ’19, Association for Computing Machinery, New York, NY, USA
(2019). https://doi.org/10.1145/3341301.3359651
45. Ma, H., Goel, A., Jeannin, J.B., Kapritsos, M., Kasikci, B., Sakallah, K.A.: Towards
automatic inference of inductive invariants. In: Proceedings of the Workshop on
Hot Topics in Operating Systems. p. 30–36. HotOS ’19, Association for Computing
Machinery, New York, NY, USA (2019). https://doi.org/10.1145/3317550.3321451
46. McMillan, K.L.: Applications of craig interpolants in model checking. In: Halbwachs, N., Zuck, L.D. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 1–12. Springer Berlin Heidelberg, Berlin, Heidelberg (2005)