BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
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 DBLP: Levin:Vladimir

Contributed to:

ASE 20112011
FASE 20112011
CAV 20102010
FASE 20102010
FASE 20042004
IFM 20042004
TACAS 20042004
CAV 20022002
FASE 20022002
ASE 20012001
CAV 20012001
TACAS 19981998

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.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.