Algebraically Provable Specification of Optimized Compilations. - Vladimir Levin (Formal Methods in Programming and Their Applications, 1993)

Verifying hardware in its software context. - Robert P. Kurshan; Vladimir Levin; Marius Minea; Doron A. Peled; Hüsnü Yenigün (ICCAD, 1997)

Verification of Message Sequence Charts via Template Matching. - Vladimir Levin; Doron A. Peled (TAPSOFT, 1997)

Static Partial Order Reduction. - Robert P. Kurshan; Vladimir Levin; Marius Minea; Doron A. Peled; Hüsnü Yenigün (TACAS, 1998)

Hazard-Freedom Checking in Speed-Independent Systems. - Hüsnü Yenigün; Vladimir Levin; Doron A. Peled; Peter A. Beerel (CHARME, 1999)

SDLcheck: A Model Checking Tool. - Vladimir Levin; Hüsnü Yenigün (CAV, 2001)

Model Checking for an Executable Subset of UML. - Fei Xie; Vladimir Levin; James C. Browne (ASE, 2001)

Compressing Transitions for Model Checking. - Robert P. Kurshan; Vladimir Levin; Hüsnü Yenigün (CAV, 2002)

ObjectCheck: A Model Checking Tool for Executable Object-Oriented Software System Designs. - Fei Xie; Vladimir Levin; James C. Browne (FASE, 2002)

Combining Software and Hardware Verification Techniques. - Robert P. Kurshan; Vladimir Levin; Marius Minea; Doron A. Peled; Hüsnü Yenigün (Formal Methods Syst. Des., 2002)

Translating Software Designs for Model Checking. - Fei Xie; Vladimir Levin; Robert P. Kurshan; James C. Browne (FASE, 2004)

SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft. - Thomas Ball 001; Byron Cook; Vladimir Levin; Sriram K. Rajamani (IFM, 2004)

Static driver verifier, a formal verification tool for Windows device drivers. - Vladimir Levin (MEMOCODE, 2004)

Automatic Creation of Environment Models via Training. - Thomas Ball 001; Vladimir Levin; Fei Xie (TACAS, 2004)

Lessons Learned from Model Checking a NASA Robot Controller. - Natasha Sharygina; James C. Browne; Fei Xie; Robert P. Kurshan; Vladimir Levin (Formal Methods Syst. Des., 2004)

Sound Transaction-Based Reduction Without Cycle Detection. - Vladimir Levin; Robert Palmer; Shaz Qadeer; Sriram K. Rajamani (SPIN, 2005)

Thorough static analysis of device drivers. - Thomas Ball 001; Ella Bounimova; Byron Cook; Vladimir Levin; Jakob Lichtenberg; Con McGarvey; Bohus Ondrusek; Sriram K. Rajamani; Abdullah Ustuner (EuroSys, 2006)

The Static Driver Verifier Research Platform. - Thomas Ball 001; Ella Bounimova; Vladimir Levin; Rahul Kumar 002; Jakob Lichtenberg (CAV, 2010)

Efficient Reachability Analysis of Büchi Pushdown Systems for Hardware/Software Co-verification. - Juncao Li; Fei Xie; Thomas Ball 001; Vladimir Levin (CAV, 2010)

An Automata-Theoretic Approach to Hardware/Software Co-verification. - Juncao Li; Fei Xie; Thomas Ball 001; Vladimir Levin; Con McGarvey (FASE, 2010)

SLAM2: Static driver verification with under 4% false alarms. - Thomas Ball 001; Ella Bounimova; Rahul Kumar 002; Vladimir Levin (FMCAD, 2010)

Model Checking Büchi Pushdown Systems. - Juncao Li; Fei Xie; Thomas Ball 001; Vladimir Levin (FASE, 2011)

Formalizing hardware/software interface specifications. - Juncao Li; Fei Xie; Thomas Ball 001; Vladimir Levin; Con McGarvey (ASE, 2011)

A decade of software model checking with SLAM. - Thomas Ball 001; Vladimir Levin; Sriram K. Rajamani (Commun. ACM, 2011)

Organizing of Parallel Processing User-Friendly Dataflow-Oriented Environment for User Tasks Execution on Cluster. - Vladimir Levin; Dmitry Kharitonov; Daria Odyakova (PaCT, 2013)

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 002; Nate Deisinger; Jakob Lichtenberg; Chetan Bansal (FMCAD, 2020)