Michael Veksler

Contact

Faculty of Industrial Engineering and Management
Technion, Israel Institute of Technology, Haifa 32000, Israel.
Technion e-mail: mveksler@tx.technion.ac.il
IBM e-mail: veksler@il.ibm.com

Education

B.Sc. Computer Engineering (Technion 1995)
Magister (IE&M Technion 2011)

Academics

I am a Ph.D. student at the IE&M faculty, working on constraint satisfaction algorithms.
My adviser is Ofer Strichman.

Research interests

Constraint solving algorithms
Proofs of CP unsatisfiablity
Formal verification

Technology (PCS)

I have implemented PCS, a Proof producing Constraint Solver, which is described in the publications below. PCS participated in the 2009 CSP competition (CSC09).

PCS is under active development.
Download information at http:///tx.technion.ac.il/~mveksler/PCS/index.html

Publications

Assumption-based pruning in conditional CSP, F. Geller and M. Veksler, in van Beek, P., ed., CP, volume 3709 of Lecture Notes in Computer Science, 241–255 © Springer-Verlag.
A Proof Producing CSP Solver, Michael Veksler and Ofer Strichman, AAAI'10

Status are related work

My research area has much recent work. At this linked page you can find references to related work and how it relates to my research.

Work

I have been working, currently part time, at IBM Research, Haifa since 1995.

Other activities

At IBM, I worked on, and led the development of a CSP solver. This solver is mainly used for automatic hardware test generation. The outcomes of this work include:

Efficient data representation of huge domain sizes (above 2⁶⁴), using DNF and BDD.
Unbounded domain size.
Efficient constraint propagation for nontrivial constraints over huge domains.
Elaborate and efficient Conditional CSP solving.

Miscellaneous:

Some mechanical work on the Wine project.
Improvements to the theorem prover CVC3 (used to be named CVC-lite)