420
A. Goel and K. Sakallah
16. Biere, A., van Dijk, T., Heljanko, K.: Hardware model checking competition 2017.
In: 2017 Formal Methods in Computer Aided Design (FMCAD). pp. 9–9. IEEE
(2017)
17. Biere, A., Preiner, M.: Hardware model checking competition (HWMCC) 2019.
http://fmv.jku.at/hwmcc19
18. Birgmeier, J., Bradley, A.R., Weissenbacher, G.: Counterexample to inductionguided abstraction-refinement (ctigar). In: Biere, A., Bloem, R. (eds.) Computer
Aided Verification. pp. 831–848. Springer International Publishing, Cham (2014)
19. Bradley, A.R.: Sat-based model checking without unrolling. In: Jhala, R., Schmidt,
D. (eds.) Verification, Model Checking, and Abstract Interpretation. pp. 70–87.
Springer Berlin Heidelberg, Berlin, Heidelberg (2011)
20. Burch, J.R., Dill, D.L.: Automatic verification of pipelined microprocessor control. In: Dill, D.L. (ed.) Computer Aided Verification. pp. 68–80. Springer Berlin
Heidelberg, Berlin, Heidelberg (1994)
21. Cabodi, G., Loiacono, C., Palena, M., Pasini, P., Patti, D., Quer, S., Vendraminetto, D., Biere, A., Heljanko, K.: Hardware model checking competition
2014: An analysis and comparison of model checkers and benchmarks. Journal
on Satisfiability, Boolean Modeling and Computation 9(1), 135–172 (Jan 2016).
https://doi.org/10.3233/SAT190106
22. Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: Ic3 modulo theories via implicit
predicate abstraction. In: ´
Abrah´ am, E., Havelund, K. (eds.) Tools and Algorithms
for the Construction and Analysis of Systems. pp. 46–61. Springer Berlin Heidelberg, Berlin, Heidelberg (2014)
23. Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: Infinite-state invariant checking
with IC3 and predicate abstraction. Formal Methods in System Design 49(3), 190–
218 (Sep 2016). https://doi.org/10.1007/s10703-016-0257-4
24. Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The mathsat5 smt solver.
In: International Conference on Tools and Algorithms for the Construction and
Analysis of Systems. pp. 93–107. Springer (2013)
25. Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) Computer Aided Verification. pp. 154–169. Springer Berlin Heidelberg, Berlin, Heidelberg (2000)
26. Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Progress on the state explosion
problem in model checking. In: Informatics. pp. 176–194. Springer (2001)
27. Clarke, E.M., Emerson, E.A., Sifakis, J.: Model checking: algorithmic verification
and debugging. Communications of the ACM 52(11), 74–84 (2009)
28. Clarke Jr, E.M., Grumberg, O., Kroening, D., Peled, D., Veith, H.: Model checking.
MIT press (2018)
29. Dureja, R., Rozier, K.Y.: Fuseic3: An algorithm for checking large design spaces.
In: 2017 Formal Methods in Computer Aided Design (FMCAD). pp. 164–171 (Oct
2017). https://doi.org/10.23919/FMCAD.2017.8102255
30. Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) Computer Aided Verification.
pp. 737–744. Springer International Publishing, Cham (2014)
31. Een, N., Mishchenko, A., Brayton, R.: Efficient implementation of property directed reachability. In: 2011 Formal Methods in Computer-Aided Design (FMCAD). pp. 125–134. IEEE (2011)
32. Ghassabani, E., Gacek, A., Whalen, M.W.: Efficient generation of inductive validity cores for safety properties. In: Proceedings of the 2016 24th ACM SIGSOFT
International Symposium on Foundations of Software Engineering. pp. 314–325
(2016)
A. Goel and K. Sakallah
16. Biere, A., van Dijk, T., Heljanko, K.: Hardware model checking competition 2017.
In: 2017 Formal Methods in Computer Aided Design (FMCAD). pp. 9–9. IEEE
(2017)
17. Biere, A., Preiner, M.: Hardware model checking competition (HWMCC) 2019.
http://fmv.jku.at/hwmcc19
18. Birgmeier, J., Bradley, A.R., Weissenbacher, G.: Counterexample to inductionguided abstraction-refinement (ctigar). In: Biere, A., Bloem, R. (eds.) Computer
Aided Verification. pp. 831–848. Springer International Publishing, Cham (2014)
19. Bradley, A.R.: Sat-based model checking without unrolling. In: Jhala, R., Schmidt,
D. (eds.) Verification, Model Checking, and Abstract Interpretation. pp. 70–87.
Springer Berlin Heidelberg, Berlin, Heidelberg (2011)
20. Burch, J.R., Dill, D.L.: Automatic verification of pipelined microprocessor control. In: Dill, D.L. (ed.) Computer Aided Verification. pp. 68–80. Springer Berlin
Heidelberg, Berlin, Heidelberg (1994)
21. Cabodi, G., Loiacono, C., Palena, M., Pasini, P., Patti, D., Quer, S., Vendraminetto, D., Biere, A., Heljanko, K.: Hardware model checking competition
2014: An analysis and comparison of model checkers and benchmarks. Journal
on Satisfiability, Boolean Modeling and Computation 9(1), 135–172 (Jan 2016).
https://doi.org/10.3233/SAT190106
22. Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: Ic3 modulo theories via implicit
predicate abstraction. In: ´
Abrah´ am, E., Havelund, K. (eds.) Tools and Algorithms
for the Construction and Analysis of Systems. pp. 46–61. Springer Berlin Heidelberg, Berlin, Heidelberg (2014)
23. Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: Infinite-state invariant checking
with IC3 and predicate abstraction. Formal Methods in System Design 49(3), 190–
218 (Sep 2016). https://doi.org/10.1007/s10703-016-0257-4
24. Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The mathsat5 smt solver.
In: International Conference on Tools and Algorithms for the Construction and
Analysis of Systems. pp. 93–107. Springer (2013)
25. Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) Computer Aided Verification. pp. 154–169. Springer Berlin Heidelberg, Berlin, Heidelberg (2000)
26. Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Progress on the state explosion
problem in model checking. In: Informatics. pp. 176–194. Springer (2001)
27. Clarke, E.M., Emerson, E.A., Sifakis, J.: Model checking: algorithmic verification
and debugging. Communications of the ACM 52(11), 74–84 (2009)
28. Clarke Jr, E.M., Grumberg, O., Kroening, D., Peled, D., Veith, H.: Model checking.
MIT press (2018)
29. Dureja, R., Rozier, K.Y.: Fuseic3: An algorithm for checking large design spaces.
In: 2017 Formal Methods in Computer Aided Design (FMCAD). pp. 164–171 (Oct
2017). https://doi.org/10.23919/FMCAD.2017.8102255
30. Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) Computer Aided Verification.
pp. 737–744. Springer International Publishing, Cham (2014)
31. Een, N., Mishchenko, A., Brayton, R.: Efficient implementation of property directed reachability. In: 2011 Formal Methods in Computer-Aided Design (FMCAD). pp. 125–134. IEEE (2011)
32. Ghassabani, E., Gacek, A., Whalen, M.W.: Efficient generation of inductive validity cores for safety properties. In: Proceedings of the 2016 24th ACM SIGSOFT
International Symposium on Foundations of Software Engineering. pp. 314–325
(2016)