Seminar - Dr. Alexandra Goultiaeva

Thursday, April 10, 2014 2:00 pm - 2:00 pm EDT (GMT -04:00)

Speaker

Dr. Alexandra Goultiaeva

Topic

Exploiting Problem Structure in QBF Solving

Abstract

Automated verification helps to build safer and more reliable systems in a shorter time. Formal verification techniques are applied widely in both hardware and software, for example, to verify the design of computer chips before they are built or to automatically generate test cases for software programs. An invaluable tool used in formal verification is a satisfiability (SAT) solver. A SAT solver finds a solution to a boolean formula, or certifies that the formula is unsolvable. Important problems in formal verification can be encoded and solved this way, and SAT solving plays a major role in the practical success of formal verification. Quantified Boolean Formula (QBF) solving is an extension of SAT solving that provides a powerful framework for encoding problems with adversarial dynamics, discrete uncertainty, or non-determinism. Improvements in QBF solving promise to widen the range of reasoning tasks that are within our reach. However, the most widely accepted formula representation format in use for QBF solving is inadequate for efficient solving. Converting to this format involves a loss of problem structure which is vital for efficient solving. In this talk, I demonstrate how structural information can be used to dramatically improve performance. I also show how the same improvement can be obtained in current QBF solvers, enabling them to have the best of both worlds. The resulting solvers benefit from the additional reasoning power provided by structural information, while retaining a widely accepted representation and the multitude of efficient techniques and data structures previously developed.

Speaker's biography

Alexandra Goultiaeva received her PhD in Computer Science from University of Toronto in 2014. Her research involves developing tools and methodologies to improve efficiency and scope of formal verification techniques. She was supported in part by the Alexander Graham Bell Scholarship with the Michael Smith Supplement which allowed her to spend a semester as a visiting researcher at the Johannes Kepler University in Linz, Austria. Alexandra's PhD research has focused on Satisfiability (SAT) and Quantified Boolean Formula (QBF) solving. She is the author of two QBF solvers, including the strongest non-CNF solver at the time of the last non-CNF QBF competition (QBFEval'10).


Invited by Professor Vijay Ganesh.