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. 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. 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.. 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), 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), 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. 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). 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. 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). 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.. 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). 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.. 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.. 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.. 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.. 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.. 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). 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), 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.. https://doi.org/10.1007/978-3-319-96142-2_16.