Publications
Main content start
Site content
- Zohar, Y., Irfan, A., Mann, M., Niemetz, A., Noetzli, A., Preiner, M., Reynolds, A., Barrett, C., & Tinelli, C. (2022). Bit-Precise Reasoning via Int-Blasting. International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2022), pp. 496-518. Springer, Cham. https://doi.org/10.1007/978-3-030-94583-1_24
- Tsiskaridze, N., Strange, M., Mann, M., Sreedhar, K., Liu, Q., Horowitz, M., & Barrett, C. (2021). Automating System Configuration. 2021 Formal Methods in Computer Aided Design (FMCAD 2021). https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_19
- Carsello, A., Thomas, J., Nayak, A., Chen, P.-H., Horowitz, M., Raina, P., & Torng, C. (2021). Enabling Reusable Physical Design Flows with Modular Flow Generators. arXiv. https://doi.org/10.48550/arXiv.2111.14535
- Stanley, D., Wang, C., Kim, S.- jin, Herbst, S., Kim, J., & Horowitz, M. (2021). Fast Validation of Mixed-Signal SoCs. IEEE Open Journal of the Solid-State Circuits Society. https://doi.org/10.1109/OJSSCS.2021.3122397
- Herbst, S., Rutsch, G., Ecker, W., & Horowitz, M. (2021). An Open-Source Framework for FPGA Emulation of Analog/Mixed-Signal Integrated Circuit Designs. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems. https://doi.org/10.1109/TCAD.2021.3102516
- Mann, M., Irfan, A., Lonsing, F., Yang, Y., Zhang, H., Brown, K., Gupta, A., & Barrett, C. (2021). Pono: a flexible and extensible SMT-based model checker. International Conference on Computer Aided Verification (CAV 2021), pp. 461-474. Springer, Cham, 2021. https://doi.org/10.1007/978-3-030-81688-9_22
- Mann, M., Wilson, A., Zohar, Y., Stuntz, L., Irfan, A., Brown, K., Donovick, C., Guman, A., Tinelli, C., & Barrett, C. (2021). SMT-switch: a solver-agnostic C++ API for SMT solving. International Conference on Theory and Applications of Satisfiability Testing (SAT 2021), pp. 377-386. Springer, Cham, 2021. https://doi.org/10.1007/978-3-030-80223-3_26
- Niemetz, A., Preiner, M., Reynolds, A., Zohar, Y., Barrett, C., & Tinelli, C. (2021). Towards Satisfiability Modulo Parametric Bit-Vectors. Journal of Automate Reasoning. JAR 65 (7): 1001-1035. http://dx.doi.org/10.1007/s10817-021-09598-9
- Huff, D., Dai, S., & Hanrahan, P. (2021). Clockwork: Resource-Efficient Static Scheduling for Multi-Rate Image Processing Applications on FPGAs. 2021 IEEE 29th Annual International Symposium on Field-Programmable Custom Computing Machines (FCCM). https://doi.org/10.1109/FCCM51124.2021.00030
- Liu, Q., Huff, D., Setter, J., Strange, M., Feng, K., Sreedhar, K., Wang, Z., Zhang, K., Horowitz, M., Raina, P., & Kjolstad, F. (2021). Compiling Halide Programs to Push-Memory Accelerators. arXiv.org. https://arxiv.org/abs/2105.12858
- Melchert, J., Feng, K., Donovick, C., Daly, R., Barrett, C., Horowitz, M., Hanrahan, P., & Raina, P. (2021). Automated Design Space Exploration of CGRA Processing Element Architectures using Frequent Subgraph Analysis. arXiv. https://doi.org/arXiv:2104.14155v1
- Mann, M., Irfan, A., Griggio, A., Padon, O., & Barrett, C. (2021). Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2021), pp. 113-132. Springer, Cham. https://doi.org/10.1007/978-3-030-72016-2_7
- Scott, J., Niemetz, A., Preiner, M., Nejati, S., & Ganesh, V. (2021). MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers. Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference (TACAS 2021) , 303–325. https://doi.org/10.1007/978-3-030-72013-1_16
- Niemetz, A., Preiner, M., Reynolds, A., Barrett, C., & Tinelli, C. (2021). Syntax-Guided Quantifier Instantiation. Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference (TACAS 2021), 145–163. https://doi.org/10.1007/978-3-030-72013-1_8
- Niemetz, A., Preiner, M., Reynolds, A., Barrett, C., & Tinelli, C. (2021). On Solving Quantified Bit-Vector Constraints using Invertibility Conditions. Formal Methods in System Design. http://dx.doi.org/10.1007/s10703-020-00359-9
- Kremer, G., Niemetz, A., & Preiner, M. (2021). ddSMT 2.0: Better Delta Debugging for the SMT-LIBv2 Language and Friends. In Proc. 33rd Int’l Conf. on Computer Aided Verification (CAV 2021). https://doi.org/10.1007/978-3-030-81688-9_11
- Kim, S.-J., Myers, Z., Herbst, S., Lim, B. C., & Horowitz, M. (2020). 20-GS/s 8b Analog-to-Digital Converter and 5-GHz Phase Interpolator for Open-Source Synthesizable High-Speed Link Applications. IEEE Solid-State Circuits Letters, 3, 518-521. https://doi.org/10.1109/LSSC.2020.3037823
- Niemetz, A., & Preiner, M. (2020). Ternary Propagation-Based Local Search for More Bit-Precise Reasoning. Formal Methods in Computer Aided Design (FMCAD). http://dx.doi.org/10.34727/2020/isbn.978-3-85448-042-6_29
- Truong, L., Herbst, S., Setaluri, R. ., Mann, M., Daly, R., Zhang, K., Donovick, C., Stanley, D., Horowitz, M., Barrett, C., & Hanrahan, P. (2020). fault: A Python Embedded Domain-Specific Language For Metaprogramming Portable Hardware Verification Components. CAV 2020: 32nd International Conference on Computer-Aided Verification July 2020. https://doi.org/10.1007/978-3-030-53288-8_19
- Bahr, R., Barrett, C., Bhagdikar, N., Carsello, A., Daly, R., Donovick, C., Durst, D., Fatahalian, K., Feng, K., Hanrahan, P., Hofstee, T., Horowitz, M., Huff, D., Kjolstad, F., Kong, T., Liu, Q., Mann, M., Melchert, J., Nayak, A., Niemetz, A., Nyengele, G., Raina, P., Richardson, S., Setaluri, R., Setter, J., Sreedhar, K., Strange, M., Thomas, J., Torng, C., Truong, L., Tsiskaridze, N., & Zhang, K. (2020). Creating an Agile Hardware Design Flow. 2020 57th ACM/IEEE Design Automation Conference (DAC). http://dx.doi.org/10.1109/DAC18072.2020.9218553