Niemetz, Aina; Preiner, Mathias; Reynolds, Andrew; Zohar, Yoni; Barrett, Clark; Tinelli, Cesare Towards satisfiability modulo parametric bit-vectors. (English) Zbl 07433026 J. Autom. Reasoning 65, No. 7, 1001-1025 (2021). MSC: 68V15 PDFBibTeX XMLCite \textit{A. Niemetz} et al., J. Autom. Reasoning 65, No. 7, 1001--1025 (2021; Zbl 07433026) Full Text: DOI
Niemetz, Aina; Preiner, Mathias; Reynolds, Andrew; Zohar, Yoni; Barrett, Clark; Tinelli, Cesare Towards bit-width-independent proofs in SMT solvers. (English) Zbl 07178987 Fontaine, Pascal (ed.), Automated deduction – CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27–30, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11716, 366-384 (2019). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{A. Niemetz} et al., Lect. Notes Comput. Sci. 11716, 366--384 (2019; Zbl 07178987) Full Text: DOI arXiv
Preiner, Mathias; Niemetz, Aina; Biere, Armin Counterexample-guided model synthesis. (English) Zbl 1452.68122 Legay, Axel (ed.) et al., Tools and algorithms for the construction and analysis of systems. 23rd international conference, TACAS 2017, held as part of the European joint conferences on theory and practice of software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017. Proceedings. Part I. Berlin: Springer. Lect. Notes Comput. Sci. 10205, 264-280 (2017). MSC: 68Q60 03B70 PDFBibTeX XMLCite \textit{M. Preiner} et al., Lect. Notes Comput. Sci. 10205, 264--280 (2017; Zbl 1452.68122) Full Text: DOI
Niemetz, Aina; Preiner, Mathias; Biere, Armin Propagation based local search for bit-precise reasoning. (English) Zbl 1377.68134 Form. Methods Syst. Des. 51, No. 3, 608-636 (2017). MSC: 68Q60 03B70 68T20 PDFBibTeX XMLCite \textit{A. Niemetz} et al., Form. Methods Syst. Des. 51, No. 3, 608--636 (2017; Zbl 1377.68134) Full Text: DOI