422
A. Goel and K. Sakallah
47. Mishchenko, A., Case, M., Brayton, R., Jang, S.: Scalable and scalably-verifiable
sequential synthesis. In: 2008 IEEE/ACM International Conference on ComputerAided Design. pp. 234–241. IEEE (2008)
48. de Moura, L., Bjørner, N.: Z3: An efficient smt solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems.
pp. 337–340. Springer Berlin Heidelberg, Berlin, Heidelberg (2008)
49. Needham, R.M., Schroeder, M.D.: Using encryption for authentication in
large networks of computers. Commun. ACM 21(12), 993–999 (Dec 1978).
https://doi.org/10.1145/359657.359659
50. Niemetz, A., Preiner, M., Biere, A.: Boolector 2.0. Journal on Satisfiability, Boolean Modeling and Computation 9(1), 53–58 (Jun 2015).
https://doi.org/10.3233/SAT190101
51. Niemetz, A., Preiner, M., Wolf, C., Biere, A.: Btor2 , btormc and boolector 3.0. In:
Chockler, H., Weissenbacher, G. (eds.) Computer Aided Verification. pp. 587–595.
Springer International Publishing, Cham (2018)
52. Pel´ anek, R.: Beem: Benchmarks for explicit model checkers. In: Boˇ snaˇ cki, D.,
Edelkamp, S. (eds.) Model Checking Software. pp. 263–267. Springer Berlin Heidelberg, Berlin, Heidelberg (2007)
53. Swamy, N., Hrit ¸cu, C., Keller, C., Rastogi, A., Delignat-Lavaud, A., Forest, S.,
Bhargavan, K., Fournet, C., Strub, P.Y., Kohlweiss, M., et al.: Dependent types
and multi-monadic effects in f. In: Proceedings of the 43rd Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages. pp. 256–270 (2016)
54. Weber, T., Conchon, S., D´ eharbe, D., Heizmann, M., Niemetz, A., Reger, G.:
The smt competition 2015 - 2018. Journal on Satisfiability, Boolean Modeling and
Computation 11(1), 221–259 (Sep 2019). https://doi.org/10.3233/SAT190123
55. Wolf, C.: Yosys open synthesis suite. http://www.clifford.at/yosys/
Open Access This chapter is licensed under the terms of the Creative Commons
Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/),
which permits use, sharing, adaptation, distribution and reproduction in any medium
or format, as long as you give appropriate credit to the original author(s) and the
source, provide a link to the Creative Commons license and indicate if changes were
made.
The images or other third party material in this chapter are included in the chapter’s
Creative Commons license, unless indicated otherwise in a credit line to the material. If
material is not included in the chapter’s Creative Commons license and your intended
use is not permitted by statutory regulation or exceeds the permitted use, you will need
to obtain permission directly from the copyright holder.
A. Goel and K. Sakallah
47. Mishchenko, A., Case, M., Brayton, R., Jang, S.: Scalable and scalably-verifiable
sequential synthesis. In: 2008 IEEE/ACM International Conference on ComputerAided Design. pp. 234–241. IEEE (2008)
48. de Moura, L., Bjørner, N.: Z3: An efficient smt solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems.
pp. 337–340. Springer Berlin Heidelberg, Berlin, Heidelberg (2008)
49. Needham, R.M., Schroeder, M.D.: Using encryption for authentication in
large networks of computers. Commun. ACM 21(12), 993–999 (Dec 1978).
https://doi.org/10.1145/359657.359659
50. Niemetz, A., Preiner, M., Biere, A.: Boolector 2.0. Journal on Satisfiability, Boolean Modeling and Computation 9(1), 53–58 (Jun 2015).
https://doi.org/10.3233/SAT190101
51. Niemetz, A., Preiner, M., Wolf, C., Biere, A.: Btor2 , btormc and boolector 3.0. In:
Chockler, H., Weissenbacher, G. (eds.) Computer Aided Verification. pp. 587–595.
Springer International Publishing, Cham (2018)
52. Pel´ anek, R.: Beem: Benchmarks for explicit model checkers. In: Boˇ snaˇ cki, D.,
Edelkamp, S. (eds.) Model Checking Software. pp. 263–267. Springer Berlin Heidelberg, Berlin, Heidelberg (2007)
53. Swamy, N., Hrit ¸cu, C., Keller, C., Rastogi, A., Delignat-Lavaud, A., Forest, S.,
Bhargavan, K., Fournet, C., Strub, P.Y., Kohlweiss, M., et al.: Dependent types
and multi-monadic effects in f. In: Proceedings of the 43rd Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages. pp. 256–270 (2016)
54. Weber, T., Conchon, S., D´ eharbe, D., Heizmann, M., Niemetz, A., Reger, G.:
The smt competition 2015 - 2018. Journal on Satisfiability, Boolean Modeling and
Computation 11(1), 221–259 (Sep 2019). https://doi.org/10.3233/SAT190123
55. Wolf, C.: Yosys open synthesis suite. http://www.clifford.at/yosys/
Open Access This chapter is licensed under the terms of the Creative Commons
Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/),
which permits use, sharing, adaptation, distribution and reproduction in any medium
or format, as long as you give appropriate credit to the original author(s) and the
source, provide a link to the Creative Commons license and indicate if changes were
made.
The images or other third party material in this chapter are included in the chapter’s
Creative Commons license, unless indicated otherwise in a credit line to the material. If
material is not included in the chapter’s Creative Commons license and your intended
use is not permitted by statutory regulation or exceeds the permitted use, you will need
to obtain permission directly from the copyright holder.