Improved Validation

Stanley, Daniel, Can Wang, Sung-jin Kim, Steven Herbst, Jaeha Kim, and Mark Horowitz. “Fast Validation of Mixed-Signal SoCs”, IEEE Open Journal of the Solid-State Circuits Society, October 25, 2021. https://doi.org/10.1109/OJSSCS.2021.3122397.

Herbst, Steven, Gabriel Rutsch, Wolfgang Ecker, and Mark Horowitz. “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, August 4, 2021. https://doi.org/10.1109/TCAD.2021.3102516.

Mann, Makai, Ahmed Irfan, Alberto Griggio, Oded Padon, and Clark Barrett. “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., March 27, 2021. https://doi.org/10.1007/978-3-030-72016-2_7.

Scott, Joseph, Aina Niemetz, Mathias Preiner, Saeed Nejati, and Vijay Ganesh. “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), March 23, 2021, 303–325. https://doi.org/10.1007/978-3-030-72013-1_16.

Niemetz, Aina, Mathias Preiner, Andrew Reynolds, Clark Barrett, and Cesare Tinelli. “Syntax-Guided Quantifier Instantiation”, Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference (TACAS 2021), March 23, 2021, 145–163. https://doi.org/10.1007/978-3-030-72013-1_8.

Niemetz, Aina, Mathias Preiner, Andrew Reynolds, Clark Barrett, and Cesare Tinelli. “On Solving Quantified Bit-Vector Constraints Using Invertibility Conditions”, Formal Methods in System Design, January 18, 2021. http://dx.doi.org/10.1007/s10703-020-00359-9.

Niemetz, Aina, and Mathias Preiner. “Ternary Propagation-Based Local Search for More Bit-Precise Reasoning”, Formal Methods in Computer Aided Design (FMCAD), September 2020. http://dx.doi.org/10.34727/2020/isbn.978-3-85448-042-6_29.

Truong, Lenny, Steven Herbst, Rajsekhar Setaluri, Makai Mann, Ross Daly, Keyi Zhang, Caleb Donovick, Daniel Stanley, Mark Horowitz, Clark Barrett, and Pat Hanrahan. “Fault: A Python Embedded Domain-Specific Language For Metaprogramming Portable Hardware Verification Components”, CAV 2020: 32nd International Conference on Computer-Aided Verification July 2020, July 21, 2020. https://doi.org/10.1007/978-3-030-53288-8_19.

Bahr, Rick, Clark Barrett, Nikhil Bhagdikar, Alex Carsello, Ross Daly, Caleb Donovick, David Durst, Kayvon Fatahalian, Kathleen Feng, Pat Hanrahan, Teguh Hofstee, Mark Horowitz, Dillon Huff, Fredrik Kjolstad, Taeyoung Kong, Qiaoyi Liu, Makai Mann, Jackson Melchert, Ankita Nayak, Aina Niemetz, Gedeon Nyengele, Priyanka Raina, Stephen Richardson, Raj Setaluri, Jeff Setter, Kavya Sreedhar, Maxwell Strange, James Thomas, Christopher Torng, Leonard Truong, Nestan Tsiskaridze, and Keyi Zhang. “Creating an Agile Hardware Design Flow”, 2020 57th ACM/IEEE Design Automation Conference (DAC), June 2020. http://dx.doi.org/10.1109/DAC18072.2020.9218553.

Mann, Makai, and Clark Barrett. “Partial Order Reduction for Deep Bug Finding in Synchronous Hardware”, International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 367-386. Springer, Cham, 2020., April 25, 2020. https://doi.org/10.1007/978-3-030-45190-5_20.

Truong, Lenny, and Pat Hanrahan. “A Golden Age of Hardware Description Languages: Applying Programming Language Techniques to Improve Design Productivity”, 3rd Summit on Advances in Programming Languages (SNAPL 2019), November 2019. https://doi.org/10.4230/LIPIcs.SNAPL.2019.7.

Niemetz, Aina, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark Barrett, and Cesare Tinelli. “Towards Bit-Width-Independent Proofs in SMT Solvers”, In: Fontaine P. (eds) Automated Deduction – CADE 27. CADE 2019. Lecture Notes in Computer Science, vol 11716. Springer, Cham., August 2019. https://doi.org/10.1007/978-3-030-29436-6_22.

Reynolds, Andrew, Andres Nötzli, Clark Barrett, and Cesare Tinelli. “High-Level Abstractions for Simplifying Extended String Constraints in SMT”, In: Dillig I., Tasiran S. (eds) Computer Aided Verification. CAV 2019. Lecture Notes in Computer Science, vol 11562. Springer, Cham., July 2019. https://doi.org/10.1007/978-3-030-25543-5_2.

Brain, Martin, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, and Cesare Tinelli. “Invertibility Conditions for Floating-Point Formulas”, In: Dillig I., Tasiran S. (eds) Computer Aided Verification. CAV 2019. Lecture Notes in Computer Science, vol 11562. Springer, Cham., July 2019. https://doi.org/10.1007/978-3-030-25543-5_8.

Ozdemir, Alex, Aina Niemetz, Mathias Preiner, Yoni Zohar, and Clark Barrett. “DRAT-Based Bit-Vector Proofs in CVC4”, In: Janota M., Lynce I. (eds) Theory and Applications of Satisfiability Testing – SAT 2019. SAT 2019. Lecture Notes in Computer Science, vol 11628. Springer, Cham., June 2019. https://doi.org/10.1007/978-3-030-24258-9_21.

Nötzli, Andres, Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Clark Barrett, and Cesare Tinelli. “Syntax-Guided Rewrite Rule Enumeration for SMT Solvers”, In: Janota M., Lynce I. (eds) Theory and Applications of Satisfiability Testing – SAT 2019. SAT 2019. Lecture Notes in Computer Science, vol 11628. Springer, Cham., June 2019. https://doi.org/10.1007/978-3-030-24258-9_20.

Huff, Dillon, and Pat Hanrahan. “Using Runtime Circuit Specialization to Accelerate Simulations of Reconfigurable Architectures”, 2018 International Conference on ReConFigurable Computing and FPGAs (ReConFig), December 2018. https://doi.org/10.1109/RECONFIG.2018.8641698.

Mattarei, Cristian, Makai Mann, Clark Barrett, Ross G. Daly, Dillon Huff, and Pat Hanrahan. “CoSA: Integrated Verification for Agile Hardware Design”, 2018 Formal Methods in Computer Aided Design (FMCAD), October 2018, 1-5. https://doi.org/10.23919/FMCAD.2018.8603014.

Niemetz, Aina, Mathias Preiner, Andrew Reynolds, Clark Barrett, and Cesare Tinelli. “Solving Quantified Bit-Vectors Using Invertibility Conditions”, In: Chockler H., Weissenbacher G. (eds) Computer Aided Verification. CAV 2018. Lecture Notes in Computer Science, vol 10982. Springer, Cham., July 2018. https://doi.org/10.1007/978-3-319-96142-2_16.