Lev Nachmanson

About

I am a Principal Research Software Development Engineer in the RISE group at Microsoft Research Redmond.

My main project is Z3 (opens in new tab), a theorem prover and constraint solver. I implemented Z3’s linear and integer arithmetic solver, a dual simplex implementation with bound propagation and cuts, modernized the nonlinear arithmetic engine, including Gröbner basis and monomial bound reasoning. Here my main collaborator is Nikolaj Bjørner.

Another area of my work is graph drawing, where I created Microsoft Automatic Graph Layout (MSAGL) (opens in new tab), a .NET set of tools graph layout and visualization, where I collaborated with Tim Dwyer, Sergey Pupyrev, Arlind Nocaj, Sergey Bereg, Alexander Holroyd, Bongshin Lee, Roman Prutkin, Christian Pich, Ted Hart: sorry if I missed somebody.

More recently I built msagljs (opens in new tab), a TypeScript port of MSAGL that runs in the browser, with SVG and deck.gl renderers, together with Xiaoji Chen, Peli de Halleux, and Assaf Shemesh. It is available on npm as @msagl/core (opens in new tab), and you can try it in the interactive demo (opens in new tab). My graph drawing research covers layered layout, edge routing and bundling, node overlap removal, and rendering of large graphs. The publication I like most is Node Overlap Removal by Growing a Tree (opens in new tab).

Earlier I worked on Spec Explorer, a model-based testing tool, where I was responsible for finite state machine visualization and graph traversal algorithms, and published on stochastic games (opens in new tab) and test strategies (opens in new tab).

Before joining Microsoft, I managed the Geometry and Kinematics team at Tecnomatix (now part of Siemens Digital Industries Software (opens in new tab)).
I received my PhD in general topology from Ural State University (now Ural Federal University (opens in new tab)) in Yekaterinburg, Russia, where I also taught calculus and general topology.

I practice CrossFit, and Ashtanga yoga: sometimes teach Ashtanga as well.