%0 Journal Article %A Maxim Petrov %A Kirill Gagarski %A Mikhail Belyaev %A Vladimir Itsykson %T Using a bounded model checker for test generation: how to kill two birds with one SMT-solver %J Modelirovanie i analiz informacionnyh sistem %D 2014 %P 83-93 %V 21 %N 6 %I mathdoc %U http://geodesic.mathdoc.fr/item/MAIS_2014_21_6_a7/ %G ru %F MAIS_2014_21_6_a7