119 citations · 168 across the 23 of their papers we have counts for
4 papers · 2 filters
Scaling Up Hardware Accelerator Verification using A-QED with Functional Decomposition
Saranyu Chattopadhyay, Florian Lonsing, Luca Piccolboni +12
Hardware accelerators (HAs) are essential building blocks for fast and energy-efficient computing systems. Accelerator Quick Error Detection (A-QED) is a recent formal technique wh…
lazybvtoint at the SMT Competition 2020
Yoni Zohar, Ahmed Irfan, Makai Mann +3
lazybvtoint is a new prototype SMT-solver, that will participate in the incremental and non-incremental tracks of the \qfbv logic.
Politeness and Stable Infiniteness: Stronger Together
Ying Sheng, Yoni Zohar, Christophe Ringeissen +3
We make two contributions to the study of polite combination in satisfiability modulo theories. The first contribution is a separation between politeness and strong politeness, by…
Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
Makai Mann, Ahmed Irfan, Alberto Griggio +2
We develop a framework for model checking infinite-state systems by automatically augmenting them with auxiliary variables, enabling quantifier-free induction proofs for systems th…