%% Holzmann G J
%
% converted from refer format by refer-to-bibtex 0.7.1
%

@phdthesis{Holzmann79,
   author = {G.J. Holzmann},
   title = {Coordination Problems in Multiprocessing Systems},
   type = {Ph.D. Thesis},
   number = {Delft Univ., The Netherlands},
   month = {June},
   year = {1979}
}

@inproceedings{Holzmann80,
   author = {G.J. Holzmann},
   editor = {D. Rayner},
   title = {The Design of Coordination Schemes},
   booktitle = {Proc. USC/ISI Workshop on Concurrency},
   address = {Idyllwild, Calif.},
   month = {March},
   year = {1980},
   note = {CSTR No. 87, Aug. 1980}
}

@inproceedings{Holzmann81,
   author = {G.J. Holzmann},
   editor = {C. Sunshine and D. Rayner},
   title = {An Algebra for Protocol Validation},
   booktitle = {Proc. 1st Int. Conf on Protocol Specification, Testing, and Verification, INWG/IFIP},
   pages = {377-391},
   address = {England},
   month = {May},
   year = {1981}
}

@techreport{Holzmann81a,
   author = {G.J. Holzmann},
   institution = {AVS Laboratory},
   title = {The Problem of the Leidsestraat - An Exercise in Process Coordination},
   type = {36},
   address = {Delft University},
   month = {August},
   year = {1981}
}

@article{Holzmann81b,
   author = {G.J. Holzmann},
   title = {Coordinatie - een net van betrouwbare processors},
   journal = {De Ingenieur},
   volume = {93},
   number = {43},
   month = {October},
   year = {1981},
   note = {In Dutch.}
}

@inproceedings{Holzmann82,
   author = {G.J. Holzmann},
   editor = {C. Sunshine},
   title = {Algebraic Validation Methods - A Comparison of Three Techniques},
   booktitle = {Proc. 2nd Int.  Conf on Protocol Specification, Testing, and Verification, INWG/IFIP},
   pages = {383--391},
   publisher = {North-Holland Publ. Co.},
   address = {Idyllwild, Calif.},
   month = {May},
   year = {1982}
}

@techreport{Holzmann82a,
   author = {G.J. Holzmann},
   institution = {AVS Laboratory},
   title = {Concise Description of a Protocol Validation Algebra},
   type = {38},
   address = {Delft University},
   month = {June},
   year = {1982}
}

@article{Holzmann82b,
   author = {G.J. Holzmann},
   title = {A Theory for Protocol Validation},
   journal = {IEEE Transactions on Computers},
   volume = {C-31},
   number = {8},
   pages = {730--738},
   month = {August},
   year = {1982}
}

@article{Holzmann83,
   author = {G.J. Holzmann},
   title = {Communicatie Protocollen - ontwerp, analyse en standaardisatie},
   journal = {Informatie},
   volume = {25},
   number = {1},
   pages = {5--11},
   month = {January},
   year = {1983},
   note = {In Dutch.}
}

@inproceedings{Holzmann83a,
   author = {G.J. Holzmann and R. A. Beukers},
   editor = {H. Rudin and C. West},
   title = {The PANDORA Protocol Development System},
   booktitle = {Proc. 3rd Int. Conf on Protocol Specification, Testing, and Verification, INWG/IFIP},
   pages = {357--369},
   publisher = {North Holland Publ. Co.},
   address = {IBM Zurich Amsterdam},
   month = {June},
   year = {1983}
}

@techreport{Holzmann83b,
   author = {G.J. Holzmann},
   institution = {AVS Laboratory},
   title = {Protocol Analysis on the PANDORA System: Four Examples},
   type = {45},
   address = {Delft University},
   month = {September},
   year = {1983}
}

@article{Holzmann83c,
   author = {G.J. Holzmann},
   title = {Systeem Krakers - Spelen Met de Computer},
   journal = {NRC Handelsblad, Science Supplement},
   month = {September},
   year = {1983},
   note = {In Dutch.}
}

@article{Holzmann84,
   author = {G.J. Holzmann},
   title = {The Unix Magician's Handbook --- a review of `The Unix Programming Environment'},
   journal = {Unix: Login},
   year = {1984}
}

@article{Holzmann84a,
   author = {G.J. Holzmann},
   title = {PANDORA - An Interactive System for the Design of Data Communication Protocols},
   journal = {Computer Networks},
   volume = {8},
   number = {2},
   pages = {71--81},
   month = {April},
   year = {1984}
}

@inproceedings{Holzmann84b,
   author = {G.J. Holzmann},
   editor = {Y. Yemini},
   title = {Backward Symbolic Execution of Protocols},
   booktitle = {Proc. 4th Int. Conf on Protocol Specification, Testing, and Verification, INWG/IFIP},
   publisher = {North Holland Publ. Co.},
   address = {Skytop, PA, USA Amsterdam},
   month = {June},
   year = {1984},
   pages = {19--30},
}

@article{Holzmann85,
   author = {G.J. Holzmann},
   title = {Tracing Protocols},
   journal = {AT\&T Technical Journal},
   volume = {64},
   number = {10},
   month = {December},
   year = {1985},
   pages = {2413--2433},
   note = {reprinted in: Current advances in distributed computation, Computer Science Press, 1986.}
}

@article{Holzmann86,
   author = {G.J. Holzmann},
   title = {Automated protocol validation in Argos, assertion proving and scatter searching},
   journal = {IEEE Trans. on Software Engineering},
   pages = {683-696},
   volume = {SE-13},
   number = {6},
   month = {June},
   year = {1986},
   note = {also in: Current advances in distributed computation, CS Press, 1986}, 
}

@incollection{Holzmann86a,
   author = {G.J. Holzmann},
   title = {Protocol Tracing,},
   booktitle = {Computer Networks and Simulation},
   volume = {III},
   publisher = {North Holland Publ. Co},
   year = {1986}
}

@techreport{Holzmann87,
   author = {G.J. Holzmann},
   title = {Manual for the protocol analyzer `Trace'},
   type = {Comp. Sci. Tech. Rep.},
   number = {134},
   month = {February},
   year = {1987},
   keywords = {CSTR},
   note = {104}
}

@article{Holzmann87a,
   author = {G.J. Holzmann},
   title = {Pico -- a picture editor},
   journal = {AT\&T Technical Journal},
   volume = {66},
   number = {2},
   pages = {2--13},
   month = {April},
   year = {1987}
}

@inproceedings{Holzmann87b,
   author = {G.J. Holzmann},
   editor = {H. Rudin and C. West},
   title = {On Limits and Possibilities of Automated Protocol Analysis},
   booktitle = {Proc. 6th Int. Conf on Protocol Specification, Testing, and Verification, INWG/IFIP},
   address = {Zurich, Sw.},
   month = {June},
   year = {1987},
   note = {(Invited paper)}
}

@article{Holzmann88,
   author = {G.J. Holzmann},
   title = {An Improved Protocol Reachability Analysis Technique},
   journal = {Software, Practice \& Experience},
   volume = {18},
   number = {2},
   pages = {137--161},
   month = {February},
   year = {1988}
}

@book{Holzmann88a,
   author = {G.J. Holzmann},
   title = {Beyond Photography --- the Digital Darkroom},
   publisher = {Prentice-Hall},
   address = {Englewood Cliffs, New Jersey},
   year = {1988}
}

@article{Holzmann88b,
   author = {G.J. Holzmann},
   title = {The Digital Darkroom},
   booktitle = {Proc. SCAN - Small Computers in the Arts Network Conference},
   month = {November},
   year = {1988},
   note = {(invited paper)}
}

@article{Holzmann89,
   author = {G.J. Holzmann},
   title = {Digital Photography},
   journal = {American Photographer},
   month = {January},
   year = {1989},
   note = {(invited paper)}
}

@inproceedings{Holzmann89a,
   author = {G.J. Holzmann and J. Patti},
   editor = {C. Vissers and E. Brinksma},
   title = {Validating SDL Specifications: An Experiment},
   booktitle = {Proc. 9th Int. Conf on Protocol Specification, Testing, and Verification, INWG/IFIP},
   address = {Twente, Neth.},
   month = {June},
   year = {1989},
   pages = {317--326},
}

@article{Holzmann90,
   author = {G.J. Holzmann},
   title = {Algorithms for Automated Protocol Verification},
   journal = {AT\&T Technical Journal},
   volume = {69},
   number = {2},
   month = {February},
   year = {1990},
   pages = {32--44},
   note = {Special Issue on Protocol Testing, Specification, and Verification}
}

@book{Holzmann91,
   author = {G.J. Holzmann},
   title = {Design and Validation of Computer Protocols},
   publisher = {Prentice-Hall},
   address = {Englewood Cliffs, New Jersey},
   year = {1991}
}

@article{Holzmann91a,
   author = {G.J. Holzmann},
   editor = {B. Pehrson and B. Jonsson and J. Parrow},
   title = {Tutorial: Design and Validation of Protocols},
   journal = {Computer Networks and ISDN Systems},
   year = {1993},
   volume = {25},
   number = {9},
   pages = {981-1017},
   note = {also in: Proc. 11th PSTV91, INWG/IFIP, Stockholm, Sweden},
}

@inproceedings{Pike91,
   author = {R. Pike, D. Presotto, K. Thompson, G.J. Holzmann},
   title = {Process Sleep and Wakeup on a Shared-memory Multiprocessor},
   booktitle = {Proc. of the Spring 1991 EurOpen Conference},
   pages = {161-166},
   address = {Tromso},
   year = {1991}
}

@article{Holzmann92,
   author = {G.J. Holzmann},
   title = {Practical Methods for the Formal Validation of SDL Specifications},
   journal = {Computer Communications},
   month = {March},
   year = {1992},
   note = {(invited paper - special issue on Practical Uses of FDT's)}
}

@article{Holzmann92a,
   author = {G.J. Holzmann},
   title = {Protocol Design: Redefining the State of the Art},
   journal = {IEEE Software},
   month = {January},
   year = {1992},
   pages = {17--22},
   note = {(invited paper - special issue on Protocol Engineering)}
}

@inproceedings{Holzmann92b,
   author = {G.J. Holzmann and P. Godefroid and D. Pirottin},
   title = {Coverage preserving reduction strategies for reachability analysis},
   booktitle = {Proc. 12th Int. Conf on Protocol Specification, Testing, and Verification, INWG/IFIP},
   address = {Orlando, Fl.},
   month = {June},
   year = {1992}
}

@article{Godefroid92,
   author = {P. Godefroid and G.J. Holzmann and D. Pirottin},
   title = {State space caching revisited},
   journal = {Formal Methods in System Design},
   month = {Nov.},
   year = {1995},
   pages = {1-15},
   publisher = {Kluwer},
   note = {also in: Proc. CAV92, Montreal, Canada},
}

@inproceedings{Laraqui92,
   author = {K. Laraqui and F. Reichert and G.J. Holzmann},
   title = {Correct design of vehicular control strategies},
   journal = {Proc 25th ISATA Int. Symp. on Automotive Techn. and Automation},
   address = {Florence, Italy},
   month = {June},
   year = {1992}
}

@article{Holzmann93,
   author = {G.J. Holzmann},
   title = {Standardizing Protocol Interfaces},
   journal = {Software Practice an Experience},
   volume = {23},
   number = {7},
   pages = {711--731},
   month = {July},
   year = {1993}
}

@inproceedings{Goderfroid93,
   author = {P. Godefroid and G.J. Holzmann},
   title = {On the verification of temporal properties},
   booktitle = {Proc. 13th Int. Conf on Protocol Specification, Testing, and Verification, INWG/IFIP},
   address = {Liege, Belgium},
   month = {May},
   year = {1993},
   pages = {109--124},
}

@article{Holzmann94,
   author = {G.J. Holzmann and B. Pehrson},
   title = {The First Data Networks},
   journal = {Scientific American},
   volume = {270},
   number = {1},
   pages = {124--129},
   month = {January},
   year = {1994}
}

@incollection{Holzmann94a,
   author = {G.J. Holzmann},
   title = {Protocol Validation},
   journal = {Encyclopedia of Telecommunications. Dekker Publ.},
   pages = {185--194},
   year = {1994}
}

@InProceedings{Holzmann94b,
   author = {G.J. Holzmann and Doron Peled},
   title = {An Improvement in Formal Verification},
   booktitle = {Proc. Formal Description Techniques, FORTE94},
   publisher = {Chapman \& Hall},
   pages = {197-211},
   address = {Berne, Switzerland},
   month = {October},
   year = {1994}
}

@inproceedings{Holzmann94c,
   author = {G.J. Holzmann},
   title = {Proving the Value of Formal Methods},
   booktitle = {Proc. FORTE94},
   address = {Berne, Switzerland},
   month = {October},
   year = {1994},
   note = {(invited paper)}
}

@inproceedings{Holzmann94d,
   author = {G.J. Holzmann},
   title = {Data Communications -- The First 2500 Years},
   booktitle = {Proc. IFIP World Computer Congress},
   address = {Hamburg, Germany},
   month = {August},
   year = {1994},
   note = {(invited paper)}
}

@inproceedings{Holzmann94e,
   author = {G.J. Holzmann},
   title = {The Theory and Practice of a Formal Method:  NewCoRe},
   booktitle = {Proc. IFIP World Computer Congress},
   address = {Hamburg, Germany},
   month = {August},
   year = {1994},
   volume = {I},
   pages = {35-44},
   publisher = {North-Holland Publ., Amsterdam, The Netherlands},
   note = {(invited paper)}
}

@book{Holzmann94f,
   author = {G.J. Holzmann and Bjorn Pehrson},
   title = {The Early History of Data Networks},
   publisher = {IEEE Computer Society Press},
   address = {Los Alamitos, California},
   month = {October},
   year = {1994}
}

@incollection{Holzmann95b,
   author = {G.J. Holzmann},
   title = {Die optische Telegraphie in England und anderen L\*:andern},
   journal = {Exhibition Catalogue, Postal Museum},
   address = {Frankfurt, Germany},
   year = {1995},
   month = {May},
   note = {(invited paper)}
}

@incollection{Holzmann95c,
   author = {G.J. Holzmann},
   title = {Geheimschrift und Zeichensprache},
   journal = {Exhibition Catalogue, Postal Museum},
   address = {Frankfurt, Germany},
   year = {1995},
   month = {May},
   note = {(invited paper)}
}

@article{Holzmann95d,
   author = {G.J. Holzmann},
   title = {The ties that bound},
   journal = {Inc. Technology},
   year = {1995},
   month = {June},
   volume = {17},
   number = {9},
   pages = {66-69},
   note = {column},
}

@inproceedings{Holzmann95e,
   author = {G.J. Holzmann},
   title = {Proving Properties of Concurrent Systems with Spin},
   booktitle = {Proc. CONCUR95, 6th Intern. Conf. on Concurrency Theory},
   address = {Philadelphia, PA.},
   year = {1995},
   month = {August},
   note = {(invited tutorial)}
}

@InProceedings{Holzmann95f,
   author = {G.J. Holzmann, D. Peled},
   title  = {Checking Linear Temporal Lgoic Properties},
   note   = {position paper},
   year   = {1995},
   booktitle = {First SPIN Workshop},
   address   = {Montr\`{e}al, Quebec},
}

@InProceedings{Holzmann95g,
   author = {G.J. Holzmann, D. Peled},
   title  = {Partial Order Reduction of the State Space},
   note   = {position paper},
   year   = {1995},
   booktitle = {First SPIN Workshop},
   address   = {Montr\`{e}al, Quebec},
}

@article{Holzmann96a,
   author = {R. Alur, G.J. Holzmann, and D. Peled},
   title = {An Analyzer for Message Sequence Charts},
   journal = {Software Concepts and Tools},
   volume = {17},
   number = {2},
   pages = {70-77},
   year = {1996},
   note = {also: Proc. TACAS95, Passau, Germany, LNCS 1055, pp. 35--48},
}

@article{Holzmann96b,
   author = {G.J. Holzmann},
   title = {Early Fault Detection Tools},
   journal = {Software Concepts and Tools},
   volume = {17},
   number = {2},
   pages = {63-69},
   year = {1996},
   note = {also: Proc. TACAS95, Passau, Germany, LNCS 1055, pp. 1-13},
}

@inproceedings{Holzmann96c,
   author = {G.J. Holzmann},
   title = {Formal Methods for Early Fault Detection},
   booktitle = {Proc. FTRTFT, Confs. on Formal Techniques for Real-Time and Fault Tolerant Systems},
   address = {Uppsala, Sweden},
   journal = {LNCS},
   volume = {1135},
   pages = {40--54},
   year = {1996},
   month = {September},
   note = {(invited paper)}
}

@inproceedings{Holzmann96d,
   author = {G.J. Holzmann, and D. Peled},
   title = {The State of Spin},
   booktitle = {8th Int. Conference on Computer Aided Verification},
   publisher = {Springer Verlag},
   series = {LNCS},
   number = {1102},
   pages = {385-389},
   year = {1996},
   address = {New Brunswick, NJ, USA},
}

@inproceedings{Holzmann96e,
   author = {G.J. Holzmann, D. Peled, and M. Yannakakis},
   title  = {On Nested Depth First Search},
   year   = {1996},
   booktitle = {The Spin Verification System},
   pages = {23-32},
   publisher = {American Mathematical Society},
   note = {Proc. of the Second Spin Workshop},
}

@inproceedings{Holzmann96f,
   author = {G.J. Holzmann, and O. Kupferman},
   title  = {Not Checking for Closure under Stuttering},
   year   = {1996},
   booktitle = {The Spin Verification System},
   pages = {17-22},
   publisher = {American Mathematical Society},
   note = {Proc. of the Second Spin Workshop},
}

@article{Holzmann96g,
   author = {J.P. Courtiat, P. Dembinski, G.J. Holzmann, L. Logrippo, Harry Rudin, and Pamela Zave},
   title  = {Formal methods after 15 years: status and trends},
   journal = {Computer Networks and ISDN Systems},
   number = {28},
   pages = {1845-1855},
   year = {1996},
   note = {Position statements of a panel discussion held at FORTE95},
}

@article{Holzmann96h,
   author = {G.J. Holzmann},
   title = {Collision Course},
   journal = {Inc. Technology},
   year = {1996},
   month = {May},
   volume = {18},
   number = {4},
   pages = {57-58},
   note = {column},
}

@Proceedings{POMIV96,
   editor = {D. Peled, V.R. Pratt, G.J. Holzmann},
   title  = {Partial Order Methods in Verification},
   year = {1997},
   volume = {29},
   series = {DIMACS series},
   publisher = {American Mathematical Society},
   note = {ISBN 0-8218-0579-7, 403pp},
}

@Proceedings{SPIN96,
   editor = {J-C Gr\'egoire, G.J. Holzmann, D. Peled},
   title  = {The Spin Verification System},
   year = {1997},
   volume = {32},
   series = {DIMACS series},
   publisher = {American Mathematical Society},
   note = {ISBN 0-8218-0680-7, 203p},
}

@article{Holzmann97a,
   author = {G.J. Holzmann},
   title  = {Designing bug-free protocols with Spin},
   year   = {1997},
   journal = {Computer Communications Journal},
   note = {invited paper},
   volume = {20},
   number = {2},
   pages = {97-105},
}

@article{Holzmann97b,
   author = {G.J. Holzmann},
   title = {An internet in the ancient world?},
   year = {1997},
   journal = {Dragonfly, a magazine for young investigators},
   number = {March/April 1997},
   pages = {22-24},
   note = {invited},
}

@article{Holzmann97c,
   author = {G.J. Holzmann, D.A. Peled, and M.H. Redberg},
   title = {Design Tools for Requirements Engineering},
   year = {1997},
   journal = {Bell Labs Technical Journal},
   month = {Winter},
   pages = {86-95},
}

@inproceedings{Holzmann97d,
   author = {G.J. Holzmann},
   title = {State Compression in Spin},
   year = {1997},
   journal = {Proc. Third Spin Workshop},
   month = {April},
   address = {Twente University, The Netherlands},
}

@article{Holzmann97e,
   author = {G.J. Holzmann},
   title = {The Model Checker Spin},
   year = {1997},
   journal = {IEEE Trans. on Software Engineering},
   month = {May},
   volume = {23},
   number = {5},
   pages  = {279-295},
   note = {Special issue on Formal Methods in Software Practice},
}

@article{Holzmann97f,
   author = {G.J. Holzmann},
   title = {Spin Model Checking},
   journal = {Dr. Dobbs Journal},
   year = {1997},
   month = {October},
}

@article{Holzmann97g,
   author = {G.J. Holzmann},
   title = {Tales of the Encrypt},
   journal = {Inc. Technology},
   volume = {19},
   number = {17},
   year = {1997},
   month = {November},
   pages  = {168},
   note = {column},
}

@inproceedings{Dershowitz97,
   author = {A. Dershowitz, K. Fisler, S. K. Shukla, G.J. Holzmann,
   R.P. Kurshan, D. Peled},
   title = {Testing the FormalCheck Query Library},
   booktitle = {Proc. LCET'96},
   organization = {Lucent Technologies},
   volume = {14},
   pages = {173-176},
   year = {1997}
}

@inproceedings{Holzmann98a,
   author = {F. Schneider, S.M. Easterbrook, J.R. Callahan, and G.J. Holzmann},
   title = {Validating Requirements for Fault Tolerant Systems using Model Checking},
   year = {1998},
   booktitle = {Proc. International Conference on Requirements Engineering, ICRE},
   month = {April},
   address = {Colorado Springs, Co., USA},
   publisher = {IEEE},
   pages = {4-14},
}

@inproceedings{Holzmann98b,
   author = {G.J. Holzmann},
   title = {Designing executable abstractions},
   journal = {Proc. Formal Methods in Software Practice},
   year = {1998},
   month = {March},
   address = {Clearwater Beach, Florida, USA},
   publisher = {ACM Press},
   note = {invited keynote address},
}

@article{Holzmann98c,
   author = {G.J. Holzmann, and Margaret H. Smith},
   title = {Interval Reduction through Requirements Analysis},
   year = {1998},
   pages = {22-31},
   note = {Bell Labs Technical Journal, Vol. 3, No. 2, 1998},
}

@article{Holzmann98d,
   author = {G.J. Holzmann},
   title = {Ports of Call},
   journal = {Inc. Technology},
   year = {1998},
   month = {March},
   volume = {20},
   number = {4},
   pages = {128},
   note = {column},
}

@article{Holzmann98e,
   author = {G.J. Holzmann},
   title = {On Checking Model Checkers},
   journal = {Proc. Computer Aided Verification Conference, LNCS 1427},
   address = {Vancouver, Canada},
   publisher = {Springer Verlag},
   year = {1998},
   month = {June},
   pages = {pp. 61-70},
   note = {invited},
}

@article{Holzmann98f,
   author = {E. Mikk, Y. Lakhnech, M. Siegel, G.J. Holzmann},
   title = {Verifying Statecharts with Spin},
   journal = {Proc. Workshop on Industrial-strength Formal specification Techniques},
   address = {Boca Raton, Fl., USA},
   year = {1998},
   month = {October},
   pages = {90-101},
   publisher = {IEEE Computer Society},
}

@article{Holzmann98g,
   author = {G.J. Holzmann},
   title = {An Analysis of Bitstate Hashing},
   journal = {Formal Methods in System Design},
   publisher = {Kluwer},
   volume = {13},
   number = {3},
   year = {1998},
   month = {November},
   pages = {287-305},
   note = {extended and revised version of Proc. PSTV95, pp. 301-314},
}

@article{Holzmann98h,
   author = {G.J. Holzmann, and Anuj Puri},
   title = {A Minimized Automaton Representation of Reachable States},
   journal = {Software Tools for Technology Transfer},
   publisher = {Springer},
   month ={November},
   year = {1999},
   volume = {2},
   number = {3},
   pages = {270-278},
}

@inproceedings{Holzmann98i,
   author = {G.J. Holzmann},
   title = {Automata Based Model Checking},
   journal = {Proc. WIFT98},
   year = {1998},
   month = {October},
   address = {Boca Raton, Fl., USA},
   note = {invited},
}

@inproceedings{Holzmann98j,
   author = {G.J. Holzmann, and Anuj Puri},
   title = {Software and Hardware Model Checking},
   journal = {Proc. ASE98},
   year = {1998},
   month = {October},
   address = {Honolulu, Hawaii, USA},
   note = {invited tutorial},
}

@inproceedings{Holzmann99a,
   author = {G.J.Holzmann, and Margaret H. Smith},
   title = {A practical method for the verification of event-driven software},
   journal = {Proc. ICSE99},
   year = {1999},
   month = {May},
   pages = {597-607},
   address = {Los Angeles, CA, USA},
}

@inproceedings{Holzmann99b,
   author = {Stefan Leue, and Gerard J. Holzmann},
   title = {V-Promela: A Visual, Object-Oriented Language for Spin},
   journal = {Proc. Second IEEE International Symposium on Object-Oriented Real-Time Distributed Computing},
   year = {1999},
   month = {May},
   address = {Saint Malo, France},
   publisher = {IEEE Computer Society Press},
}

@article{Holzmann99c,
   author = {G.J. Holzmann},
   title = {Castles in the air},
   journal = {Inc. Technology},
   year = {1999},
   month = {May},
   volume = {21},
   number = {4},
   pages = {128},
   note = {column},
}

@inproceedings{Holzmann99d,
   author = {G.J. Holzmann},
   title = {The engineering of a model checker: the Gnu i-protocol case study revisited},
   journal = {Proc. of the 6th Spin Workshop / LNCS },
   publisher = {Springer Verlag},
   volume = {LNCS 1680},
   year = {1999},
   month = {Sept.},
   address = {Toulouse, France},
}

@inproceedings{HS99,
   author = {G.J. Holzmann, and Margaret H. Smith},
   title = {Software model checking - Extracting verification models from source code},
   journal = {Formal Methods for Protocol Engineering and Distributed Systems},
   year = {1999},
   month = {Oct.},
   address = {Kluwer Academic Publ.},
   pages = {481-497},
   note = {also in: Software Testing, Verification and Reliability, Vol. 11, No. 2, June 2001, pp. 65-79.},
}

@article{Holzmann99e,
   author = {G.J. Holzmann},
   title = {Taking Stock},
   journal = {Inc. Technology},
   year = {1999},
   month = {November},
   volume = {21},
   number = {13},
   pages = {156},
   note = {column},
}

@article{Holzmann00a,
   author = {G.J. Holzmann},
   title = {Software verification at Bell Labs: one line of development},
   journal = {Bell Labs Technical Journal},
   volume = {5},
   number = {1},
   month ={Jan-March},
   year = {2000},
   pages = {35-45},
   note = {Bell Labs 75th year anniversary issue},
}

@article{HS00a,
   author = {G.J. Holzmann, and Margaret H. Smith},
   title = {Automating software feature verification},
   journal = {Bell Labs Technical Journal},
   volume = {5},
   number = {2},
   month ={April-June},
   year = {2000},
   pages = {72-87},
   note = {Issue on Software Complexity},
}

@article{Holzmann00b,
   author = {G.J. Holzmann},
   title = {Outside the box},
   journal = {Inc. Technology},
   year = {2000},
   month = {May},
   volume = {22},
   number = {1},
   pages = {164},
   note = {column},
}

@article{Holzmann00c,
   author = {G.J. Holzmann},
   title = {Tallying Up},
   journal = {Inc. Technology},
   year = {2000},
   month = {July},
   volume = {22},
   number = {2},
   pages = {196},
   note = {column},
}

@inproceedings{KH00,
   author = {K. Etessami and G.J. Holzmann},
   title = {Optimizing Buchi automata},
   journal = {Proc. CONCUR2000 },
   publisher = {Springer Verlag / LNCS 1877},
   pages = {153-167},
   year = {2000},
   month = {Aug.},
}

@inproceedings{Holzmann00d,
   author = {G.J. Holzmann},
   title = {Logic Verification of ANSI-C Code with Spin},
   journal = {Proc. SPIN2000},
   publisher = {Springer Verlag / LNCS 1885},
   year = {2000},
   pages = {131-147},
   month = {Sep.},
}

@article{Holzmann00e,
   author = {G.J. Holzmann},
   title = {Machinations},
   journal = {Inc. Technology},
   year = {2000},
   month = {Sept.},
   volume = {22},
   number = {3},
   pages = {176},
   note = {column},
}

@article{Holzmann00f,
   author = {G.J. Holzmann},
   title = {MEMS the word},
   journal = {Inc. Technology},
   year = {2000},
   month = {Nov.},
   volume = {22},
   number = {3},
   note = {column},
}

@incollection{Holzmann00g,
   author = {G.J. Holzmann},
   title = {Software Model Checking},
   journal = {NATO Summer School},
   address = {Marktoberdorf, Germany},
   year = {2000},
   month = {Aug.},
   publisher = {IOS Press, Computer and System Sciences },
   volume = {180},
   pages = {309-355},
}

@incollection{Holzmann00h,
   author = {G.J. Holzmann},
   title = {Using Spin - introduction to a tool for analyzing parallel and distributed programs},
   journal = {Plan 9, Programmer's Manual, Documents},
   address = {York, England},
   year = {2000},
   publisher = {Vita Nuova Holdings Ltd},
   pages = {353-382},
}

@inproceedings{SHE01,
   author = {M.H. Smith, G.J. Holzmann, and K. Etessami},
   title = {Events and Constraints, a graphical editor for capturing logic properties of programs},
   journal = {Proc. 5th International Symposium on Requirements Engineering},
   address = {Toronto, Canada},
   pages = {14-22},
   year = {2001},
   month = {Aug.},
}

@inproceedings{Holzmann01a,
   author = {G.J. Holzmann},
   title = {From Code to Models},
   journal = {Proc. 2nd Int. Conf. on Applications of Concurrency to System Design},
   address = {Newcastle upon Tyne, U.K.},
   pages = {3-10},
   year = {2001},
   month = {June},
}

@inproceedings{Holzmann01b,
   author = {G.J. Holzmann},
   title = {Economics of Software Verification},
   journal = {Proc. Workshop on Program Analysis for Software Tools and Engineering},
   address = {Snowbird, Utah, USA},
   publisher = {ACM},
   year = {2001},
   month = {June},
}

@inproceedings{Holzmann02a,
   author = {Peter R. Gluck (NASA/JPL), G.J. Holzmann},
   title = {Using Spin Model Checking for Flight Software Verification},
   journal = {Proc. 2002 Aerospace Conference},
   address = {Big Sky, MT, USA},
   publisher = {IEEE},
   year = {2002},
   month = {March},
}

@inproceedings{Holzmann02b,
   author = {G.J. Holzmann},
   title = {Static source code checking for user-defined properties},
   journal = {Proc. IDPT 2002},
   address = {Pasadena, CA, USA},
   year = {2002},
   month = {June},
}

@article{Holzmann02c,
   author = {G.J.Holzmann, and Margaret H. Smith},
   title = {An automated verification method for distributed systems software based on model extraction},
   journal = {IEEE Trans. on Software Engineering},
   volume = {28},
   number = {4},
   year = {2002},
   month = {April},
   pages = {364-377},
}

@inproceedings {DHH02,
   author = {D. Dams, W. Hesse, G.J. Holzmann},
   title = {Abstracting C with abC},
   journal = {Proc. CAV 2002},
   address = {Copenhagen, Denmark},
   publisher = {Springer Verlag, LNCS},
   year = {2002},
   month = {July},
}

@inproceedings {Holzmann02d,
   author = {G.J. Holzmann},
   title = {Software Analysis and Model Checking},
   journal = {Proc. CAV 2002},
   address = {Copenhagen, Denmark},
   year = {2002},
   month = {July},
}

@inproceedings {Holzmann02e,
   author = {G.J. Holzmann},
   title = {The Logic of Bugs},
   journal = {Proc. ACM Foundations of Software Engineering, FSE 2002},
   address = {Charleston, SC, USA},
   year = {2002},
   month = {November},
}

@book{Holzmann03,
   author = {G.J. Holzmann},
   title = {The Spin Model Checker, Primer and Reference Manual},
   publisher = {Addison-Wesley},
   address = {Reading, Massachusetts},
   year = {2003}
}