PhD Thesis Proposal, Vasilis Papavasileiou, 2014. [PDF]
We present the Mathematical Programming Modulo Theories (MPMT) constraint solving framework. MPMT enhances Mathematical Programming technology by integrating techniques from the field of Automated Reasoning, e.g., solvers for first-order theories. We study the theoretical aspects of MPMT by means of the Branch and Cut Modulo T (BC(T)) transition system. BC(T) can be thought of as a blueprint for MPMT solvers. We outline classes of first-order theories that BC(T) can accommodate. We discuss the design and implementation of a BC(T)-based solver for MPMT. Finally, we explore applications in aerospace and databases.
Panagiotis (Pete) Manolios, Professor, College of Computer and Information Science, Northeastern University (Advisor)
Eugene Goldberg, Research Assistant Professor, College of Computer and Information Science, Northeastern University
Mirek Riedewald, Associate Professor, College of Computer and Information Science, Northeastern University
Thomas Wahl, Assistant Professor, College of Computer and Information Science, Northeastern University
Leonardo de Moura, Principal Researcher, Research in Software Engineering (RiSE) Group, Microsoft Research (External Member)
Thomas and Eugene are the FM experts on the faculty. Mirek brings expertise in big data. Leonardo de Moura is one of the leading researchers in SMT and is the author of Z3, one of the most widely used SMT solvers. -- Pete