| 2020 | FMCAD | Angelic Checking within Static Driver Verifier: Towards high-precision defects without (modeling) cost. | Shuvendu K. Lahiri, Akash Lal, Sridhar Gopinath, Alexander Nutz, Vladimir Levin, Rahul Kumar, Nate Deisinger, Jakob Lichtenberg, Chetan Bansal |
| 2013 | PACT | Organizing of Parallel Processing User-Friendly Dataflow-Oriented Environment for User Tasks Execution on Cluster. | Vladimir Levin, Dmitry Kharitonov, Daria Odyakova |
| 2011 | FASE | Model Checking Bchi Pushdown Systems. | Juncao Li, Fei Xie, Thomas Ball, Vladimir Levin |
| 2010 | CAV | The Static Driver Verifier Research Platform. | Thomas Ball, Ella Bounimova, Vladimir Levin, Rahul Kumar, Jakob Lichtenberg |
| 2010 | CAV | Efficient Reachability Analysis of Bchi Pushdown Systems for Hardware/Software Co-verification. | Juncao Li, Fei Xie, Thomas Ball, Vladimir Levin |
| 2010 | FASE | An Automata-Theoretic Approach to Hardware/Software Co-verification. | Juncao Li, Fei Xie, Thomas Ball, Vladimir Levin, Con McGarvey |
| 2010 | FMCAD | SLAM2: Static driver verification with under 4% false alarms. | Thomas Ball, Ella Bounimova, Rahul Kumar, Vladimir Levin |
| 2006 | EuroSys | Thorough static analysis of device drivers. | Thomas Ball, Ella Bounimova, Byron Cook, Vladimir Levin, Jakob Lichtenberg, Con McGarvey, Bohus Ondrusek, Sriram K. Rajamani, Abdullah Ustuner |
| 2004 | FASE | Translating Software Designs for Model Checking. | Fei Xie, Vladimir Levin, Robert P. Kurshan, James C. Browne |
| 2004 | IFM | SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft. | Thomas Ball, Byron Cook, Vladimir Levin, Sriram K. Rajamani |
| 2004 | MEMOCODE | Static driver verifier, a formal verification tool for Windows device drivers. | Vladimir Levin |
| 2004 | TACAS | Automatic Creation of Environment Models via Training. | Thomas Ball, Vladimir Levin, Fei Xie |
| 2002 | CAV | Compressing Transitions for Model Checking. | Robert P. Kurshan, Vladimir Levin, Hsn Yenign |
| 2002 | FASE | ObjectCheck: A Model Checking Tool for Executable Object-Oriented Software System Designs. | Fei Xie, Vladimir Levin, James C. Browne |
| 2001 | CAV | SDLcheck: A Model Checking Tool. | Vladimir Levin, Hsn Yenign |
| 1998 | TACAS | Static Partial Order Reduction. | Robert P. Kurshan, Vladimir Levin, Marius Minea, Doron A. Peled, Hsn Yenign |
| 1997 | ICCAD | Verifying hardware in its software context. | Robert P. Kurshan, Vladimir Levin, Marius Minea, Doron A. Peled, Hsn Yenign |