Resolution Proofs and Skolem Functions in QBF Evaluation and Applications. - Valeriy Balabanov; Jie-Hong R. Jiang (CAV, 2011)

TSV-aware analytical placement for 3D IC designs. - Meng-Kai Hsu; Yao-Wen Chang; Valeriy Balabanov (DAC, 2011)

Henkin Quantifiers and Boolean Formulae. - Valeriy Balabanov; Hui-Ju Katherine Chiang; Jie-Hong Roland Jiang (SAT, 2012)

Unified QBF certification and its applications. - Valeriy Balabanov; Jie-Hong R. Jiang (Formal Methods Syst. Des., 2012)

TSV-Aware Analytical Placement for 3-D IC Designs Based on a Novel Weighted-Average Wirelength Model. - Meng-Kai Hsu; Valeriy Balabanov; Yao-Wen Chang (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2013)

QBF Resolution Systems and Their Proof Complexities. - Valeriy Balabanov; Magdalena Widl; Jie-Hong R. Jiang (SAT, 2014)

Henkin quantifiers and Boolean formulae: A certification perspective of DQBF. - Valeriy Balabanov; Hui-Ju Katherine Chiang; Jie-Hong R. Jiang (Theor. Comput. Sci., 2014)

Efficient Extraction of QBF (Counter)models from Long-Distance Resolution Proofs. - Valeriy Balabanov; Jie-Hong Roland Jiang; Mikolas Janota; Magdalena Widl (AAAI, 2015)

Speeding up MUS Extraction with Preprocessing and Chunking. - Valeriy Balabanov; Alexander Ivrii (SAT, 2015)

Clauses Versus Gates in CEGAR-Based 2QBF Solving. - Valeriy Balabanov; Jie-Hong Roland Jiang; Alan Mishchenko; Christoph Scholl 001 (AAAI Workshop: Beyond NP, 2016)

2QBF: Challenges and Solutions. - Valeriy Balabanov; Jie-Hong Roland Jiang; Christoph Scholl 001; Alan Mishchenko; Robert K. Brayton (SAT, 2016)

Flexibility and Optimization of QBF Skolem-Herbrand Certificates. - Valeriy Balabanov; Shuo-Ren Lin; Jie-Hong R. Jiang (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2016)