Travelled to:
1 × Cyprus
1 × Denmark
1 × Germany
1 × Portugal
2 × France
2 × Spain
2 × USA
2 × United Kingdom
Collaborated with:
F.Xie T.Ball H.Yenigün J.C.Browne J.Li R.P.Kurshan D.A.Peled C.McGarvey B.Cook S.K.Rajamani E.Bounimova R.Kumar J.Lichtenberg M.Minea D.Peled
Talks about:
model (7) check (7) softwar (5) hardwar (3) system (3) static (3) verif (3) pushdown (2) verifi (2) object (2)
Person: Vladimir Levin
DBLP: Levin:Vladimir
Contributed to:
Wrote 14 papers:
- ASE-2011-LiXBLM #formal method #hardware #interface #specification
- Formalizing hardware/software interface specifications (JL, FX, TB, VL, CM), pp. 143–152.
- FASE-2011-LiXBL #automaton #model checking
- Model Checking Büchi Pushdown Systems (JL, FX, TB, VL), pp. 141–155.
- CAV-2010-BallBLKL #framework #platform #research #verification
- The Static Driver Verifier Research Platform (TB, EB, VL, RK, JL), pp. 119–122.
- CAV-2010-LiXBL #analysis #automaton #hardware #performance #reachability
- Efficient Reachability Analysis of Büchi Pushdown Systems for Hardware/Software Co-verification (JL, FX, TB, VL), pp. 339–353.
- FASE-2010-LiXBLM #approach #hardware
- An Automata-Theoretic Approach to Hardware/Software Co-verification (JL, FX, TB, VL, CM), pp. 248–262.
- FASE-2004-XieLKB #design #model checking
- Translating Software Designs for Model Checking (FX, VL, RPK, JCB), pp. 324–338.
- IFM-2004-BallCLR #formal method #verification
- SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft (TB, BC, VL, SKR), pp. 1–20.
- TACAS-2004-BallLX #automation #modelling
- Automatic Creation of Environment Models via Training (TB, VL, FX), pp. 93–107.
- CAV-2002-KurshanLY #model checking
- Compressing Transitions for Model Checking (RPK, VL, HY), pp. 569–581.
- FASE-2002-XieLB #design #execution #model checking #named #object-oriented
- ObjectCheck: A Model Checking Tool for Executable Object-Oriented Software System Designs (FX, VL, JCB), pp. 331–335.
- ASE-2001-XieLB #execution #model checking #set #uml
- Model Checking for an Executable Subset of UML (FX, VL, JCB), pp. 333–336.
- CAV-2001-LevinY #model checking #named
- SDLcheck: A Model Checking Tool (VL, HY), p. 377.
- TACAS-1998-KurshanLMPY #partial order #reduction
- Static Partial Order Reduction (RPK, VL, MM, DP, HY), pp. 345–357.
- TAPSOFT-1997-LevinP #sequence chart #verification
- Verification of Message Sequence Charts via Template Matching (VL, DAP), pp. 652–666.