% Generated by IEEEtran.bst, version: 1.12 (2007/01/11)
\begin{thebibliography}{10}
\providecommand{\url}[1]{#1}
\csname url@samestyle\endcsname
\providecommand{\newblock}{\relax}
\providecommand{\bibinfo}[2]{#2}
\providecommand{\BIBentrySTDinterwordspacing}{\spaceskip=0pt\relax}
\providecommand{\BIBentryALTinterwordstretchfactor}{4}
\providecommand{\BIBentryALTinterwordspacing}{\spaceskip=\fontdimen2\font plus
\BIBentryALTinterwordstretchfactor\fontdimen3\font minus
  \fontdimen4\font\relax}
\providecommand{\BIBforeignlanguage}[2]{{%
\expandafter\ifx\csname l@#1\endcsname\relax
\typeout{** WARNING: IEEEtran.bst: No hyphenation pattern has been}%
\typeout{** loaded for the language `#1'. Using the pattern for}%
\typeout{** the default language instead.}%
\else
\language=\csname l@#1\endcsname
\fi
#2}}
\providecommand{\BIBdecl}{\relax}
\BIBdecl

\bibitem{cobleigh01}
J.~{C}obleigh, L.~{C}larke, and L.~{O}sterweil, ``{T}he {R}ight {A}lgorithm at
  the {R}ight {T}ime: {C}omparing {D}ata {F}low {A}nalysis {A}lgorithms for
  {F}inite-{S}tate {V}erification,'' in \emph{{P}roc. {I}nternational
  {C}onference on {S}oftware {E}ngineering}, 2001.

\bibitem{owen07}
D.~{O}wen, ``{C}ombining {C}omplementary {F}ormal {V}erification {S}trategies
  to {I}mprove {P}erformance and {A}ccuracy,'' Ph.D. dissertation, {W}est
  {V}irginia {U}niversity, 2007.

\bibitem{owen02a}
------, ``{R}andom {S}earch of {AND}-{OR} {G}raphs {R}epresenting
  {F}inite--{S}tate {M}odels,'' Master's thesis, {W}est {V}irginia
  {U}niversity, 2002.

\bibitem{menzies02}
T.~{M}enzies, D.~{O}wen, and B.~{C}ukic, ``{S}aturation {E}ffects in {T}esting
  of {F}ormal {M}odels,'' in \emph{{P}roc. {I}nternational {S}ymposium on
  {S}oftware {R}eliability {E}ngineering}, 2002.

\bibitem{owen02c}
D.~{O}wen, B.~{C}ukic, and T.~{M}enzies, ``{A}n {A}lternative to {M}odel
  {C}hecking: {V}erification by {R}andom {S}earch of {AND}-{OR} {G}raphs
  {R}epresenting {F}inite-{S}tate {M}odels,'' in \emph{{P}roc. {I}nternational
  {S}ymposium on {H}igh-{A}ssurance {S}ystems {E}ngineering}, 2002.

\bibitem{owen02b}
D.~{O}wen, T.~{M}enzies, and B.~{C}ukic, ``{W}hat {M}akes {F}inite-{S}tate
  {M}odels {M}ore (or less) {T}estable?'' in \emph{{P}roc. {I}nternational
  {C}onference on {A}utomated {S}oftware {E}ngineering}, 2002.

\bibitem{owen03a}
D.~{O}wen and T.~{M}enzies, ``{L}urch: a {L}ightweight {A}lternative to {M}odel
  {C}hecking,'' in \emph{{P}roc. {I}nternational {C}onference of {S}oftware
  {E}ngineering and {K}nowledge {E}ngineering}, 2003.

\bibitem{holzmann03}
G.~{H}olzmann, \emph{{T}he {SPIN} {M}odel {C}hecker}.\hskip 1em plus 0.5em
  minus 0.4em\relax {A}ddison-{W}esley, 2003.

\bibitem{mcmillan00}
K.~{M}cMillan, ``{T}he {SMV} {S}ystem,'' 2000, available at
  \url{www.kenmcmil.com/tutorial.ps}.

\bibitem{owen03b}
D.~{O}wen, T.~{M}enzies, M.~{H}eimdahl, and J.~{G}ao, ``{O}n the {A}dvantages
  of {A}pproximate vs. {C}omplete {V}erification: {B}igger {M}odels, {F}aster,
  {L}ess {M}emory, {U}sually {A}ccurate,'' in \emph{{P}roc. {IEEE} / {NASA}
  {S}oftware {E}ngineering {W}orkshop}, 2003.

\bibitem{owen06}
D.~{O}wen, D.~{D}esovski, and B.~{C}ukic, ``{E}ffectively {C}ombining
  {S}oftware {V}erification {S}trategies: {U}nderstanding {D}ifferent
  {A}ssumptions,'' in \emph{{P}roc. {I}nternational {S}ymposium on {S}oftware
  {R}eliability {E}ngineering}, 2006.

\bibitem{heitmeyer05}
C.~{H}eitmeyer, M.~{A}rcher, R.~{B}haradwaj, and R.~{J}effords, ``{T}ools for
  {C}onstructing {R}equirements {S}pecifications: {T}he {SCR} {T}oolset at the
  {A}ge of {T}en,'' \emph{{C}omputer {S}ystems {S}cience and {E}ngineering},
  vol.~20, no.~1, 2005.

\bibitem{huth00}
M.~{H}uth and M.~{R}yan, \emph{{L}ogic in {C}omputer {S}cience: {M}odelling and
  {R}easoning {A}bout {S}ystems}.\hskip 1em plus 0.5em minus 0.4em\relax
  {C}ambridge {U}niversity {P}ress, 2000.

\bibitem{holzmann97}
G.~{H}olzmann, ``{T}he {M}odel {C}hecker {SPIN},'' \emph{{IEEE} {T}ransactions
  on {S}oftware {E}ngineering}, vol.~23, no.~5, 1997.

\bibitem{clarke99}
E.~{C}larke, O.~{G}rumberg, and D.~{P}eled, \emph{{M}odel {C}hecking}.\hskip
  1em plus 0.5em minus 0.4em\relax {MIT} {P}ress, 1999.

\bibitem{cimatti00}
A.~{C}imatti, E.~{C}larke, F.~{G}iunchiglia, and M.~{R}overi, ``{N}u{SMV}: {A}
  {N}ew {S}ymbolic {M}odel {C}hecker,'' \emph{{I}nternational {J}ournal on
  {S}oftware {T}ools for {T}echnology {T}ransfer}, vol.~2, no.~4, 2000.

\bibitem{havelund00}
K.~{H}avelund, M.~{L}owry, J.~{P}enix, W.~{V}isser, and J.~{W}hite, ``{F}ormal
  {A}nalysis of the {R}emote {A}gent {B}efore and {A}fter {F}light,'' in
  \emph{{P}roc. {NASA} {L}angley {F}ormal {M}ethods {W}orkshop}, 2000.

\bibitem{gluck02}
P.~{G}l{\"{u}}ck and G.~{H}olzmann, ``{U}sing {SPIN} {M}odel {C}hecking for
  {F}light {S}oftware {V}erification,'' in \emph{{P}roc. {IEEE} {A}erospace
  {C}onference}, 2002.

\bibitem{holzmann04}
G.~{H}olzmann and R.~{J}oshi, ``{M}odel-{D}riven {S}oftware {V}erification,''
  in \emph{{P}roc. {I}nternational {SPIN} {W}orkshop on {M}odel {C}hecking of
  {S}oftware}, 2004.

\bibitem{ball01}
T.~{B}all and S.~{R}ajamani, ``{A}utomatically {V}alidating {T}emporal {S}afety
  {P}roperties of {I}nterfaces,'' \emph{{L}ecture {N}otes in {C}omputer
  {S}cience}, vol. 2057, 2001.

\bibitem{holzmann90}
G.~{H}olzmann, \emph{{D}esign and {V}alidation of {C}omputer
  {P}rotocols}.\hskip 1em plus 0.5em minus 0.4em\relax {P}rentice {H}all, 1990.

\bibitem{holzmann87}
------, ``{A}utomated {P}rotocal {V}alidation in {A}rgos: {A}ssertion {P}roving
  and {S}catter {S}earching,'' \emph{{IEEE} {T}ransactions on {S}oftware
  {E}ngineering}, vol.~13, no.~6, 1987.

\bibitem{biere99}
A.~{B}iere, A.~{C}imatti, E.~{C}larke, and Y.~{Z}hu, ``{S}ymbolic {M}odel
  {C}hecking {W}ithout {BDD}s,'' \emph{{L}ecture {N}otes in {C}omputer
  {S}cience}, vol. 1579, 1999.

\bibitem{groce02}
A.~{G}roce and W.~{V}isser, ``{H}euristic {M}odel {C}hecking for {J}ava
  {P}rograms,'' in \emph{{P}roc. {I}nternational {SPIN} {W}orkshop on {M}odel
  {C}hecking of {S}oftware}, 2002.

\bibitem{dong03}
Y.~{D}ong, X.~{D}u, G.~{H}olzmann, and S.~{S}molka, ``{F}ighting {L}ivelock in
  the {GNU} i-{P}rotocol: a {C}ase {S}tudy in {E}xplicit-{S}tate {M}odel
  {C}hecking,'' \emph{{I}nternational {J}ournal on {S}oftware {T}ools for
  {T}echnology {T}ransfer}, vol.~4, no.~4, 2003.

\bibitem{gargantini99}
A.~{G}argantini and C.~{H}eitmeyer, ``{U}sing {M}odel {C}hecking to {G}enerate
  {T}ests from {R}equirements {S}pecifications,'' in \emph{{P}roc. {J}oint
  {E}uropean {S}oftware {E}ngineering {C}onference and {ACM} {S}igsoft
  {I}nternational {S}ymposium on {F}oundations of {S}oftware {E}ngineering},
  1999.

\bibitem{heimdahl03}
M.~{H}eimdahl, S.~{R}ayadurgam, W.~{V}isser, G.~{D}evaraj, and J.~{G}ao,
  ``{A}uto-{G}enerating {T}est {S}equences {U}sing {M}odel {C}heckers: {A}
  {C}ase {S}tudy,'' in \emph{{P}roc. {I}nternational {W}orkshop on {F}ormal
  {A}pproaches to {T}esting of {S}oftware}, 2003.

\bibitem{savage97}
S.~{S}avage, M.~{B}urrows, G.~{N}elson, P.~{S}obalvarro, and T.~{A}nderson,
  ``{E}raser: {A} {D}ynamic {D}ata {R}ace {D}etector for {M}ultithreaded
  {P}rograms,'' \emph{{ACM} {T}ransactions on {C}omputer {S}ystems}, vol.~15,
  no.~4, 1997.

\bibitem{godefroid97}
P.~{G}odefroid, ``{M}odel {C}hecking for {P}rogramming {L}anguages {U}sing
  {V}erisoft,'' in \emph{{P}roc. {S}ymposium on {P}rinciples of {P}rogramming
  {L}anguages}, 1997.

\bibitem{sims01}
S.~{S}ims, R.~{C}leaveland, K.~{B}utts, and S.~{R}anville, ``{A}utomated
  {V}alidation of {S}oftware {M}odels,'' in \emph{{P}roc. {I}nternational
  {C}onference on {A}utomated {S}oftware {E}ngineering}, 2001.

\bibitem{corbett96}
J.~{C}orbett, ``{E}valuating {D}eadlock {D}etection {M}ethods for {C}oncurrent
  {S}oftware,'' \emph{{IEEE} {T}ransactions on {S}oftware {E}ngineering},
  vol.~22, no.~3, 1996.

\bibitem{bharadwaj99}
R.~{B}haradwaj and C.~{H}eitmeyer, ``{M}odel {C}hecking {C}omplete
  {R}equirements {S}pecifications {U}sing {A}bstraction,'' \emph{{A}utomated
  {S}oftware {E}ngineering}, vol.~6, no.~1, 1999.

\bibitem{west89}
C.~{W}est, ``{P}rotocol {V}alidation in {C}omplex {S}ystems,'' \emph{{ACM}
  {SIGCOMM} {C}omputer {C}ommunication {R}eview}, vol.~19, no.~4, 1989.

\bibitem{chockler06}
H.~{C}hockler, O.~{K}upferman, and M.~{V}ardi, ``{C}overage {M}etrics for
  {T}emporal {L}ogic {M}odel {C}hecking,'' \emph{{F}ormal {M}ethods in {S}ystem
  {D}esign}, vol.~28, 2006.

\bibitem{bharadwaj00}
R.~{B}haradwaj and S.~{S}ims, ``{C}ombining {C}onstraint {S}olvers with {BDD}s
  for {A}utomatic {I}nvariant {C}hecking,'' in \emph{{P}roc. {T}ools and
  {A}lgorithms for the {C}onstruction and {A}nalysis of {S}ystems}, 2000.

\bibitem{archer02}
M.~{A}rcher, C.~{H}eitmeyer, and E.~{R}iccobene, ``{P}roving {I}nvariants of
  {I}/{O} {A}utomata with {TAME},'' \emph{{A}utomated {S}oftware
  {E}ngineering}, vol.~9, no.~3, 2002.

\bibitem{cimatti02}
A.~{C}imatti, E.~{C}larke, E.~{G}iunchiglia, F.~{G}iunchiglia, M.~{P}istore,
  M.~{R}overi, R.~{S}ebastiani, and A.~{T}acchella, ``{NuSMV2}: {A}n
  {O}pen-{S}ource {T}ool for {S}ymbolic {M}odel {C}hecking,'' in \emph{{P}roc.
  {I}nternational {C}onference on {C}omputer-{A}ided {V}erification}, 2004.

\bibitem{nsa03}
``{R}equirements {S}pecification for {P}ersonnel {A}ccess {C}ontrol {S}ystem.
  {N}ational {S}ecurity {A}gency,'' 2003.

\bibitem{widmaier00}
J.~{Widmaier}, C.~{S}midts, and X.~{H}uang, ``{P}roducing {M}ore {R}eliable
  {S}oftware: {M}ature {S}oftware {E}ngineering {P}rocess vs.
  {S}tate-of-the-{A}rt {T}echnology?'' in \emph{{P}roc. {I}nternational
  {C}onference on {S}oftware {E}ngineering}, 2000.

\bibitem{desovski06}
D.~{D}esovski, ``{A} {C}omponent-{B}ased {A}pproach to {V}erification and
  {V}alidation of {F}ormal {S}oftware {M}odels,'' Ph.D. dissertation, {W}est
  {V}irginia {U}niversity, 2006.

\bibitem{offutt96}
A.~{O}ffutt, A.~{L}ee, G.~{R}othermel, R.~{U}ntch, and C.~{Z}apf, ``{A}n
  {E}xperimental {D}etermination of {S}ufficient {M}utant {O}perators,''
  \emph{{ACM} {T}ransactions of {S}oftware {E}ngineering {M}ethodology},
  vol.~5, no.~2, 1996.

\bibitem{andrews06}
J.~{A}ndrews, L.~{B}riand, Y.~{L}abiche, and A.~{N}amin, ``{U}sing {M}utation
  {A}nalysis for {A}ssessing and {C}omparing {T}esting {C}overage {C}riteria,''
  \emph{{IEEE} {T}ransactions on {S}oftware {E}ngineering}, vol.~32, no.~8,
  2006.

\end{thebibliography}