bibliography



Books

[link] The Spin Model Checker - Primer and Reference Manual
G.J. Holzmann
Addison-Wesley, Reading Massachusetts, 2004, ISBN 0-321-22862-6, 608 pgs.
[link] The Early History of Data Networks
G.J. Holzmann and B. Pehrson
IEEE Computer Society Press, Los Alamitos CA, (John Wiley & Sons), Oct. 1994.
[link] Design and Validation of Computer Protocols
G.J. Holzmann
Prentice-Hall, Englewood Cliffs New Jersey, 1991.
[link] Beyond Photography - the Digital Darkroom
G.J. Holzmann
Prentice-Hall, Englewood Cliffs New Jersey, 1988.

Proceedings

[link] Proc. 7th NASA Formal Methods Symposium
K. Havelund, G. Holzmann, R. Joshi (Eds)
Springer Verlag, LNCS 9058, 2015, ISBN 978-3-319-17524-9.
[link] Proc. 3rd NASA Formal Methods Symposium
M. Bobaru, K. Havelund, G. Holzmann, R. Joshi (Eds)
Springer Verlag, LNCS 6617, 2011, ISBN 978-3-642-20398-5.
[link] The Spin Verification System
J-C Gregoire, G.J. Holzmann, and D. Peled (Eds)
American Mathematical Society, DIMACS Series, Vol. 32, 1997, ISBN 0-8218-0680-7, 203 pgs.
[link] Partial Order Methods in Verification
D. Peled, V.R. Pratt, and G.J. Holzmann (Eds)
American Mathematical Society, DIMACS Series, Vol. 29, 1997, ISBN 0-8218-0579-7, 403 pgs.


Papers, Columns, etc.


2023
[PDF] Programming Event Monitors,
K. Havelund and G.J. Holzmann
Software Tools for Technology Transfer, 2013, to appear.
[PDF] Exploring File Systems for Input Coverage
Y. Liu, G.J. Holzmann, G. Kuenning, S. Smolka, E. Zadok
Proc. FAST'23, Usenix Conf on File and Storage Technologies.

2021
[PDF] Model-Checking Support for File System Development
W. Su, Y. Liu, G. Ganesan, G.J. Holzmann, G. Kuenning, S. Smolka, E. Zadok
Proc. HotStorage '21, Position paper, July 2021, 7 pgs.
[PDF] A Programming Approach to Log Analysis
Klaus Havelund and G.J. Holzmann
30 pgs, (to appear).
[PDF] Comparing Two Methods for Checking Runtime Properties
G.J. Holzmann
6 pgs, (to appear).
[PDF] Keeping it Simple: Agile Analysis
G.J. Holzmann
IEEE Software, column on Reliable Code, Vol. 38, No. 3 (2021), pp. tbd.
[PDF] Right Code
G.J. Holzmann
IEEE Software, column on Reliable Code, Vol. 38, No. 1 (2021), pp. 13-15.

2020
[PDF] Predicting the Past
G.J. Holzmann
IEEE Software, column on Reliable Code,Vol. 37, No. 2 (2020), pp. 10-12.
[PDF] Test Fatigue
G.J. Holzmann
IEEE Software, column on Reliable Code,Vol. 37, No. 4 (2020), pp. 11-16.

2019
[PDF] Formalizing Requirements is <>[] Hard
G.J. Holzmann
From Reactive Systems to Cyber-Physical Systems,
Eds E. Bartocci, R. Cleaveland, R. Grosu, O. Sokolsky,
LNCS, Springer-Verlag, August 2019.
[PDF] Code Overload
G.J. Holzmann
IEEE Software, column on Reliable Code, Nov/Dec 2019, pp. 73-75.
[PDF] Does Not Compute
G.J. Holzmann
IEEE Software, column on Reliable Code, May/Jun 2019, pp. 14-16.
[PDF] Code Mining
G.J. Holzmann
IEEE Software, column on Reliable Code, Mar/Apr 2019, pp. 25-29.

2018
[PDF] Code Vault
G.J. Holzmann
IEEE Software, column on Reliable Code, Sept/Oct 2018, pp. 2-4.
[PDF] Software Components
G.J. Holzmann
IEEE Software, column on Reliable Code, May/June 2018, pp. 2-4.
[PDF] Curve Balls
G.J. Holzmann
IEEE Software, column on Reliable Code, March/April 2018, pp. 2-5.
[PDF] Ends and Means
G.J. Holzmann
IEEE Software, column on Reliable Code, Jan/Feb 2018, pp. 2-5.

2017
[PDF] Randomly Right
G.J. Holzmann
IEEE Software, column on Reliable Code, Sep/Oct 2017, pp. 2-4.
[PDF] Cobra: Fast Structural Code Checking
G.J. Holzmann
Proc. 24th Int. Spin Symposium, July 2017, UC Santa Barbara, CA.
Pub. ACM DOI: 10.1145/3092282.3092313.
[PDF] Dead Programs
G.J. Holzmann
IEEE Software, column on Reliable Code, Jul/Aug 2017, pp. tbd.
[PDF] A Tale of Three Programs
G.J. Holzmann
IEEE Software, column on Reliable Code, May/Jun 2017, pp. 67-70.
[PDF] Code Craft
G.J. Holzmann
IEEE Software, column on Reliable Code, Mar/Apr 2017, pp. 18-21.
[PDF] The Value of Doubt
G.J. Holzmann
IEEE Software, column on Reliable Code, Jan/Feb 2017, pp. 106-109.

2016
[PDF]
[preprint]
Cobra: a light-weight tool for static and dynamic program analysis
G.J. Holzmann
Innovations in Systems and Software Engineering, a NASA Journal,
online: DOI 10.1007/s11334-016-0282-x, June 2016.
print: Vol. 13, Issue 1, pp. 35-49, March 2017.
[PDF] Hi Maintenance
G.J. Holzmann
IEEE Software, column on Reliable Code, Nov/Dec 2016, pp. 98-101.
[PDF] Brace Yourself
G.J. Holzmann
IEEE Software, column on Reliable Code, Sept/Oct 2016, pp. 12-15.
[PDF] The Weakest Link
G.J. Holzmann
IEEE Software, column on Reliable Code, July/August 2016, pp. 12-15.
[PDF] Frequently Unanswered Questions
G.J. Holzmann
IEEE Software, column on Reliable Code, May/June 2016, pp. 10-12.
[PDF] Code Clarity
G.J. Holzmann
IEEE Software, column on Reliable Code, Mar./Apr. 2016, pp. 22-25.
[PDF] Tiny Tools
G.J. Holzmann
IEEE Software, column on Reliable Code, Jan./Feb. 2016, pp. 24-28.
[PDF] Cloud-based verification of concurrent software
G.J. Holzmann
Proc. VMCAI 2016, St. Petersburg, Fl., Jan. 2016. Springer-Verlag, LNCS.

2015
[PDF] Out of Bounds
G.J. Holzmann
IEEE Software, column on Reliable Code, Nov/Dec. 2015, pp. 24-26.
[PDF] Code Evasion
G.J. Holzmann
IEEE Software, column on Reliable Code, Sep/Oct. 2015, pp. 77-80.
[PDF] Points of Truth
G.J. Holzmann
IEEE Software, column on Reliable Code, July/Aug. 2015, pp. 18-21.
[PDF] A multi-paradigm languange for reactive synthesis
I. Filippidis, R.M. Murray, and G.J. Holzmann
Proc. 4th Workshop on Synthesis, SYNT 2015, July 2015.
[PDF] Assertive Testing
G.J. Holzmann
IEEE Software, column on Reliable Code, May/June 2015, pp. 12-15.
[PDF] Code Inflation
G.J. Holzmann
IEEE Software, column on Reliable Code, March/Apr. 2015, pp. 10-13.
[PDF] To Code is Human
G.J. Holzmann
IEEE Software, column on Reliable Code, Jan/Feb. 2015, pp. 16-19.

2014
[PDF] Fault Intolerance
G.J. Holzmann
IEEE Software, column on Reliable Code, Nov/Dec. 2014, pp. 16-20.
[PDF] Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning
A. Groce, K. Havelund, G.J. Holzmann, R. Joshi, R-G Xu
Annals of Mathematics and Artificial Intelligence, 2014, Vol. 70, No. 4, pp. 315-349.
[PDF]
[erratum]
Mars Code
G.J. Holzmann
Communications of the ACM, Vol. 57, No. 2, Feb. 2014, pp. 64-73, (cover article, downloaded over 100K times in first 10 months).
[PDF] An improvement of the piggyback algorithm for parallel model checking
Ioannis Filippidis and G.J. Holzmann
Proc. Int. Spin Symposium on Model Checking of Software, July 2014, CA, ACM Press, pp. 48-57.

2013
[PDF] Proving Properties of Concurrent Programs
G.J. Holzmann
Proc. 20th Spin Workshop / Symposium, July 2013, Springer, LNCS 7976, pp 18-23.
[PDF] A Three-Step Program for Recovering Hackers
G.J. Holzmann
IEEE Computer, June 2013, pp. 10-12.
[PDF] Landing a Spacecraft on Mars
G.J. Holzmann
IEEE Software, Impact Column, Mar./Apr. 2013, pp. 17-20.

2012
[PDF] Parallelizing the Spin Model Checker
G.J. Holzmann
Proc. 19th Int. Spin Workshop, Oxford, England, July 2012, Springer, LNCS 7385, pp. 155-171.
[PDF] Logic model checking of time-periodic real-time systems
M. Florian, E. Gamble, G.J. Holzmann,
Proc. Infotech@Aerospace Conference, AIAA, Garden Grove, CA, June 2012 (invited).

2011
[PDF] Model checking multitask applications for OSEK compliant real-time operating systems
M. McKelvin, and G.J. Holzmann
Proc. 17th IEEE Pacific Rim Int. Symposium on Dependable Computing (PRDC 2011)
Pasadena, CA, Dec. 12-14, 2011.
[PDF] Swarm Verification Techniques
G.J. Holzmann, R. Joshi, A. Groce
IEEE Trans. on Software Engineering, Vol. 37, No. 6, Nov/Dec 2011, pp. 845-857.
[PDF] Software Certification - Coding, code, and coders
K. Havelund, and G.J. Holzmann
Proc. Int. Conf. on Embedded Software, EMSOFT'11, Oct. 2011, Taipei, Taiwan (invited).
[PDF] Reliable software development: analysis aware design
G.J. Holzmann
Proc. European Joint Conferences on Theory and Practice of Software (ETAPS), keynote
Saarbrucken, Germany, Apr. 2011.
[PDF] Model checking with bounded context switching
G.J. Holzmann, M. Florian
Formal Aspects of Computing, 2011, Vol. 23, Issue 3, p. 365-389.

2010
[PDF] Scrub: a tool for code reviews
G.J. Holzmann
Innovations in Systems and Software Engineering, 2010, Vol. 6, Nr. 4, pp. 311-318.

2009
[PDF] Experience Using the Power of Ten Coding Rules
Michael McDougal and G.J. Holzmann
Software Test & Performance Magazine, Vol. 6, No. 10, Oct. 2009, pp. 12-16.

2008
[PDF] Model driven code checking
G.J. Holzmann, R. Joshi, A. Groce
Automated Software Engineering Journal,
Vol. 15, Nr. 3-4, Dec. 2008, pp. 283-297.
[PDF] Software Safety and Rocket Science
G.J. Holzmann
ECRIM News 75, On Safety-critical software, European Research Consortium for Informatics and Mathematics, Oct. 2008.
[PDF] Swarm Verification
G.J. Holzmann, R. Joshi, A. Groce
Proc. ASE 2008, 23rd IEEE/ACM Int. Conf. on Automated Software Engineering, l'Aquila, Italy, Sept. 2008.
[PDF] Tackling large verification problems with the Swarm tool
G.J. Holzmann, R. Joshi, A. Groce
15th Spin Workshop, UCLA, Los Angeles, Aug. 2008, LNCS 5156, pp. 134-143.
[PDF] Putting flight software through the paces with testing, model checking, and constraint solving
A. Groce, G.J. Holzmann, R. Joshi, R. Xu
Proc. Int. Workshop on Constraints in Formal Verification, Sydney, Australia, Aug. 2008.
[PDF] Automated testing of planning models
K. Havelund, A. Groce, G.J. Holzmann, R. Joshi, M. Smith
Proc. Workshop on Model Checking and Artificial Intelligence, Patras, Greece, July 2008.

2007
[PDF] Conquering Complexity
G.J. Holzmann
IEEE Computer, Dec. 2007.
[slides]
[link]
The Design of a multi-core extension of the Spin Model Checker
G.J. Holzmann and Dragan Bosnacki
(first presented at: Formal Methods in Computer Aided Design (FMCAD), San Jose, Nov. 2006.)
IEEE Trans. on Software Engineering, Vol. 33, No. 10, pp. 659-674, Oct. 2007.
[PDF]
[link]
A Stack-Slicing Algorithm for Multi-Core Model Checking
G.J. Holzmann
Proc. PDMC 2007, Berlin, July 8, 2007 (also in: Electronic Notes in Theoretical Computer Science, 2008).
[PDF] A mini challenge: build a verifiable filesystem
R. Joshi and G.J. Holzmann
Proc. Verified Software: Theories, Tools, Experiments, Zurich, Sw., Oct. 2005, Springer Verlag, LNCS 4171, pp. 49-56.
also in: Formal Aspects of Computing, 2007, Vol. 19, 4 pgs.
[PDF] Randomized differential testing as a prelude to formal verification
A. Groce, G.J. Holzmann, R. Joshi
Proc. ICSE 2007, Minneapolis, US, May 20-26, 2007.
[PDF]
[link]
Multi-core model checking with Spin
G.J. Holzmann and Dragan Bosnacki
Proc. HIPS-TopModels 2007, Long Beach, Mar. 26-30, 2007, (short paper)

2006
[abs]
[PDF]
New Challenges in Model Checking
G.J. Holzmann, R. Joshi, A. Groce
Proc. Symposium 25 Years of Model Checking, Federated Logic Conference (FLOC),
Seattle, Aug. 2006. Publ. LNCS Vol. 5000, pp. 65-76, 2008.
[PDF]
[PDF orig]
The Power of Ten: Rules for Developing Safety Critical Code
G.J. Holzmann
IEEE Computer, June 2006

2005
[PDF] Reliable Software Systems Design
G.J. Holzmann and R. Joshi
Proc. Verified Software: Theories, Tools, Experiments,
Zurich, Sw., Oct. 2005, Springer Verlag, LNCS 4171, pp. 237-244.
[PDF] Improving Spin's partial-order reduction for breadth-first search
D. Bosnacki and G.J. Holzmann
Proc. 12th Int. Spin Workshop, San Francisco, Aug. 2005, Springer Verlag, LNCS 3639, pp. 91-105.
[PDF] Software Model Checking with Spin
G.J. Holzmann
in: Advances in Computers, Vol. 65, Ed. M. Zelkowitz, Elsevier Publ., Amsterdam, pp.77-108, July 2005.
[PDF] Model checking artificial intelligence based planners
M.H. Smith, G. Cucullu, G.J. Holzmann, and B. Smith
Proc. 2005 Aerospace Conf., IEEE, Big Sky MT USA, Mar. 2005.

2004
[PDF] Model-Driven Software Verification
G.J. Holzmann and R. Joshi
Proc. 11th Spin Workshop, Barcelona, Spain, Apr. 2004, Springer Verlag, LNCS 2989, pp. 77-92.

2003
[PDF] Trends in Software Verification
G.J. Holzmann
Proc. Formal Methods Europe Conference, Pisa, Italy, Sept. 2003.
[PDF] Fighting livelock in the GNU i-protocol: a case study in explicit-state model checking
Yifei Dong, Xiaoqun Du, G.J. Holzmann, S.A. Smolka
Software Tools for Technology Transfer, 2003, Vol. 4, No. 4, pp. 505-528.

2002
[PDF] The Logic of Bugs
G.J. Holzmann
Proc. ACM Foundations of Software Engineering FSE 2002, Charleston SC USA, Nov. 2002.
[PDF] Validation of mission critical software design and implementation using model checking
P. Pingree, E. Mikk, G. Holzmann, M. Smith, and D. Dams
Proc. 21st Digital Avionics Systems Conference, Vol. 1, Oct. 2002, pp. 6A4:1-12.
[PDF] Software Analysis and Model Checking
G.J. Holzmann
Proc. CAV 2002, Copenhagen Denmark, July 2002.
[PDF] Abstracting C with abC
D. Dams, W. Hesse, and G.J. Holzmann
Proc. CAV 2002, Springer Verlag LNCS 2404, Copenhagen Denmark, July 2002, pp. 515-520.
[PDF] Static source code checking for user-defined properties
G.J. Holzmann
Proc. IDPT 2002, Pasadena CA USA, June 2002.
[PDF] An automated verification method for distributed systems software based on model extraction
G.J. Holzmann and M.H. Smith
IEEE Trans. on Software Engineering, Vol. 28, No. 4, pp. 364-377, Apr. 2002.
[PDF] Using Spin Model Checking for Flight Software Verification
P.R. Gluck and G.J. Holzmann
Proc. 2002 Aerospace Conference, IEEE, Big Sky MT USA, Mar. 2002.

2001
[PDF] Events and Constraints a graphical editor for capturing logic properties of programs
M.H. Smith G.J. Holzmann and K. Etessami
Proc. 5th International Symposium on Requirements Engineering, pp. 14-22, Toronto Canada, Aug. 2001.
[PDF] From Code to Models
G.J. Holzmann
Proc. 2nd Int. Conf. on Applications of Concurrency to System Design, pp. 3-10, Newcastle upon Tyne U.K., June 2001.
[PDF] Economics of Software Verification
G.J. Holzmann
Proc. Workshop on Program Analysis for Software Tools and Engineering, ACM, Snowbird Utah USA, June 2001.

2000
[link] MEMS the word
G.J. Holzmann
Inc. Technology, Vol. 22, No. 3, Nov. 2000, (column).
[link] And the credit goes to
G.J. Holzmann
Inc. Technology, Vol. 22, No. 3, pp. 176, Sept. 2000, (column).
[PDF] Logic Verification of ANSI-C Code with Spin
G.J. Holzmann
Proc. SPIN2000, Sep. 2000, Springer Verlag LNCS 1885, pp. 131-147.
[PDF] Software Model Checking
G.J. Holzmann
NATO Summer School, Vol. 180, pp. 309-355,
IOS Press Computer and System Sciences, Marktoberdorf Germany, Aug. 2000.
[PDF] Optimizing Buchi automata
K. Etessami and G.J. Holzmann
Proc. CONCUR2000, Aug. 2000, Springer Verlag LNCS 1877, pp. 153-167.
[link] Tallying Up
G.J. Holzmann
Inc. Technology, Vol. 22, No. 2, pp. 196, July 2000, (column).
[PDF] Automating software feature verification
G.J. Holzmann and M.H. Smith
Bell Labs Technical Journal, Vol. 5, No. 2, pp. 72-87, Apr.-Jun. 2000.
(Special Issue on Software Complexity).
[link] Outside the box
G.J. Holzmann
Inc. Technology, Vol. 22, No. 1, pp. 164, May 2000, (column).
[PDF] Software verification at Bell Labs: one line of development
G.J. Holzmann
Bell Labs Technical Journal, Vol. 5, No. 1, pp. 35-45, Jan.-Mar. 2000.
(Bell Labs 75th year anniversary issue).
[PDF] Using Spin
G.J. Holzmann
Plan 9 Programmer s Manual Documents, pp. 353-382, Vita Nuova Holdings Ltd, York England.
1st edition 1995, 2nd edition, 2000.

1999
[PDF] A Minimized Automaton Representation of Reachable States
G.J. Holzmann and Anuj Puri
Software Tools for Technology Transfer, Vol. 2, No. 3, pp. 270-278, Springer, Nov. 1999.
[link] Taking Stock
G.J. Holzmann
Inc. Technology, Vol. 21, No. 13, pp. 156, Nov. 1999, (column).
[PDF] Software model checking - Extracting verification models from source code
G.J. Holzmann and M.H. Smith
Formal Methods for Protocol Engineering and Distributed Systems, pp. 481-497, Kluwer Academic Publ., Oct. 1999,
(also in: Software Testing Verification and Reliability Vol. 11 No. 2 June 2001 pp. 65-79). [PDF]
[PDF] The engineering of a model checker: the Gnu i-protocol case study revisited
G.J. Holzmann
Proc. of the 6th Spin Workshop, Toulouse France, Sept. 1999, LNCS 1680, Springer Verlag, pp. 232-244.
[PDF] A practical method for the verification of event-driven software
G.J. Holzmann and M.H. Smith
Proc. ICSE99, pp. 597-607, Los Angeles CA USA, May 1999.
[link] Castles in the air
G.J. Holzmann
Inc. Technology, Vol. 21, No. 4, pp. 128, May 1999, (column).
[PDF] V-Promela: A Visual Object-Oriented Language for Spin
S. Leue and G.J. Holzmann
Proc. Second IEEE International Symposium on Object-Oriented Real-Time Distributed Computing, IEEE Computer Society Press, Saint Malo France, May 1999.

1998
[PDF] An Analysis of Bitstate Hashing
G.J. Holzmann
Formal Methods in System Design, Vol. 13, No. 3, pp. 287-305, Kluwer, Nov. 1998.
(extended and revised version of Proc. PSTV95 pp. 301-314).
[PDF] Automata Based Model Checking
G.J. Holzmann
Proc. WIFT98, Boca Raton Fl. USA, Oct. 1998, (invited).
[PDF] Hardware and Software Model Checking
G.J. Holzmann and Anuj Puri
Proc. ASE98, Honolulu Hawaii USA, Oct. 1998, (invited tutorial).
[PDF] Implementing Statecharts in Promela/Spin
E. Mikk, Y. Lakhnech, M. Siegel, and G.J. Holzmann
Proc. Workshop on Industrial-strength Formal specification Techniques, pp. 90-101, Boca Raton Fl. USA, IEEE Computer Society, Oct. 1998.
[link] Just the Fax
G.J. Holzmann
Inc. Technology, Vol. 20, Sept 1998, (column).
[PDF] On Checking Model Checkers
G.J. Holzmann
Proc. Computer Aided Verification Conference, Springer Verlag, LNCS 1427, pp. 61-70, Vancouver Canada, June 1998, (invited).
[PDF] Validating Requirements for Fault Tolerant Systems using Model Checking
F. Schneider S.M. Easterbrook J.R. Callahan and G.J. Holzmann
Proc. Int. Conf. on Requirements Engineering ICRE, pp. 4-14, IEEE, Colorado Springs Co. USA, Apr. 1998.
[PDF] Designing executable abstractions
G.J. Holzmann
Proc. Formal Methods in Software Practice, ACM Press, Clearwater Beach Florida USA, Mar. 1998, (invited keynote address).
[link] Ports of Call
G.J. Holzmann
Inc. Technology, Vol. 20, No. 4, pp. 128, Mar. 1998, (column).
[PDF] Interval Reduction through Requirements Analysis
G.J. Holzmann, and M.H. Smith
Bell Labs Technical Journal, Vol. 3, No. 2, pp. 22-31, 1998.

1997
[PDF] Design Tools for Requirements Engineering
G.J. Holzmann, D. Peled, and M.H. Redberg
Bell Labs Technical Journal, pp. 86-95, Winter 1997.
[link] Tales from the Encrypt
G.J. Holzmann
Inc. Technology, Vol. 19, No. 17, pp. 168, Nov. 1997, (column).
[PDF] Reliable Design of Concurrent Software
G.J. Holzmann
Dr. Dobbs Journal, Oct. 1997.
[PDF] Testing the FormalCheck Query Library
A. Dershowitz, K. Fisler, S. K. Shukla, G.J. Holzmann, R.P. Kurshan, D. Peled
Proc. LCET 96, Vol. 14, pp. 173-176, Lucent Technologies, 1997.
[PDF] Designing bug-free protocols with Spin
G.J. Holzmann
Computer Communications Journal, Vol. 20, No. 2, pp. 97-105, 1997, (invited paper).
[PDF] The Model Checker Spin
G.J. Holzmann
IEEE Trans. on Software Engineering, Vol. 23, No. 5, pp. 279-295, May 1997.
(Special issue on Formal Methods in Software Practice).
[PDF] State Compression in Spin
G.J. Holzmann
Proc. Third Spin Workshop, Twente University, The Netherlands, Apr. 1997.
[PDF] An internet in the ancient world?
G.J. Holzmann
Dragonfly a magazine for young investigators, Mar.-Apr. 1997, pp. 22-24, 1997, (invited).
[link] Outline for an operational semantics of Promela
V. Natarajan, and G.J. Holzmann
American Mathematical Society, DIMACS Series, Vol. 32, 1997, pp. 133-152.

1996
[PDF] Formal Methods for Early Fault Detection
G.J. Holzmann
Proc. FTRTFT Confs. on Formal Techniques for Real-Time and Fault Tolerant Systems,
LNCS 1135, pp. 40-54, Uppsala Sweden, Sept. 1996, (invited paper).
[link] Collision Course
G.J. Holzmann
Inc. Technology, Vol. 18, No. 4, pp. 57-58, May 1996, (column).
[PDF] The State of Spin
G.J. Holzmann and D. Peled
Proc. 8th Int. Conference on Computer Aided Verification,
Springer Verlag, LNCS 1102, pp. 385-389, New Brunswick NJ USA, 1996.
[PDF] On Nested Depth First Search
G.J. Holzmann, D. Peled, and M. Yannakakis
Proc. of the 2nd Spin Workshop. The Spin Verification System, pp. 23-32,
American Mathematical Society, 1996.
[PDF] Not Checking for Closure under Stuttering
G.J. Holzmann, and O. Kupferman
Proc. of the 2nd Spin Workshop. The Spin Verification System, pp. 17-22,
American Mathematical Society, 1996.
[link] Formal methods after 15 years: status and trends
J.P. Courtiat, P. Dembinski, G.J. Holzmann, L. Logrippo, Harry Rudin, and Pamela Zave
Computer Networks and ISDN Systems, Vol. 28, pp. 1845-1855, 1996.
(Position statements of a panel discussion held at FORTE95).
[PDF] An Analyzer for Message Sequence Charts
R. Alur, G.J. Holzmann and D. Peled
Software Concepts and Tools, Vol. 17, No. 2, pp. 70-77, 1996.
(also: Proc. TACAS95, Passau, Germany, LNCS 1055, Springer Verlag, pp. 35-48).
[PDF] Early Fault Detection Tools
G.J. Holzmann
Software Concepts and Tools, Vol. 17, No. 2, pp. 63-69, 1996.
(also: Proc. TACAS95, Passau, Germany, LNCS 1055, Springer Verlag, pp. 1-13).

1995
[PDF] State space caching revisited
P. Godefroid, G.J. Holzmann, and D. Pirottin
Formal Methods in System Design, pp. 1-15, Kluwer, Nov. 1995,
(also in: Proc. CAV92, Montreal, Canada).
[PDF] Proving Properties of Concurrent Systems with Spin
G.J. Holzmann
Proc. CONCUR95 6th Intern. Conf. on Concurrency Theory,
Philadelphia PA., Aug. 1995, (invited tutorial).
[link] The ties that bound
G.J. Holzmann
Inc. Technology, Vol. 17, No. 9, pp. 66-69, June 1995, (column).
[english] Die optische Telegraphie in England und anderen Landern
G.J. Holzmann
Exhibition Catalogue Postal Museum, Frankfurt Germany, May 1995, (invited contribution).
[english] Geheimschrift und Zeichensprache
G.J. Holzmann
Exhibition Catalogue Postal Museum, Frankfurt Germany, May 1995, (invited contribution).
[PDF] Checking Linear Temporal Lgoic Properties
G.J. Holzmann and D. Peled First SPIN Workshop, Montreal Quebec, 1995, (position paper).

1994
[PDF] Proving the Value of Formal Methods
G.J. Holzmann
Proc. Formal Description Techniques FORTE94, Berne, Switzerland, Oct. 1994, (invited paper).
[PDF] An Improvement in Formal Verification
G.J. Holzmann and D. Peled
Proc. Formal Description Techniques FORTE94, Berne, Switzerland, pp. 197-211, Chapman Hall, Berne, Switzerland, Oct. 1994.
[PDF] The Theory and Practice of a Formal Method: NewCoRe
G.J. Holzmann
Proc. IFIP World Computer Congress, Vol. I, pp. 35-44, Hamburg Germany, Aug. 1994, North-Holland Publ. Amsterdam The Netherlands. (invited paper).
[PDF] Data Communications - The First 2500 Years
G.J. Holzmann
Proc. IFIP World Computer Congress, Hamburg Germany, Aug. 1994, (Invited paper).
[link] The First Data Networks
G.J. Holzmann and B. Pehrson
Scientific American, Vol. 270, No. 1, pp. 124-129, Jan. 1994.
[PDF] Protocol Validation
G.J. Holzmann
Encyclopedia of Telecommunications. Dekker Publ., pp. 185-194, 1994.

1993
[PDF] Hype - A Hypertext Browser
G.J. Holzmann
AT&T Bell Laboratories Technical Memorandum TM-11271-930909-05, Sept. 1993.
[PDF] Standardizing Protocol Interfaces
G.J. Holzmann
Software Practice and Experience, Vol. 23, No. 7, pp. 711-731, July 1993.
[PDF] On the verification of temporal properties
P. Godefroid and G.J. Holzmann
Proc. 13th Int. Conf on Protocol Specification Testing and Verification INWG IFIP, pp. 109-124, Liege Belgium, May 1993.
[PDF] Tutorial: Design and Validation of Protocols
G.J. Holzmann
Ed. B. Pehrson and B. Jonsson and J. Parrow,
Computer Networks and ISDN Systems, Vol. 25, No. 9, pp. 981-1017, 1993.
(also in: Proc. 11th PSTV91 INWG IFIP Stockholm Sweden).

1992
[PDF]
(15MB)
Tutorial: Design and Validation of Protocols
G.J. Holzmann
International Conference on Network Protocols (ICNP), San Franciscom CA, Oct. 19-22, 1993.
[PDF] Correct design of vehicular control strategies
K. Laraqui and F. Reichert, and G.J. Holzmann
Proc 25th ISATA Int. Symp. on Automotive Techn. and Automation, Florence Italy, June 1992.
[PDF] Coverage preserving reduction strategies for reachability analysis
G.J. Holzmann, P. Godefroid, and D. Pirottin
Proc. 12th Int. Conf on Protocol Specification Testing and Verification,
INWG IFIP, Orlando Fl., June 1992.
[PDF] Practical Methods for the Formal Validation of SDL Specifications
G.J. Holzmann
Computer Communications, Mar. 1992.
(Invited paper - special issue on Practical Uses of FDTs.)
[PDF] Protocol Design: Redefining the State of the Art
G.J. Holzmann
IEEE Software, pp. 17-22, Jan. 1992.
(Invited paper - special issue on Protocol Engineering.)

1991
[PDF] Process Sleep and Wakeup on a Shared-memory Multiprocessor
R. Pike, D. Presotto, K. Thompson, and G.J. Holzmann
Proc. of the Spring 1991 EurOpen Conference, pp. 161-166, Tromso, 1991.

1990
[PDF] Algorithms for Automated Protocol Verification
G.J. Holzmann
AT&T Technical Journal, Vol. 69, No. 2, pp. 32-44, Feb. 1990.
(Special Issue on Protocol Testing Specification and Verification).

1989
[PDF] Validating SDL Specifications: An Experiment
G.J. Holzmann and J. Patti
Proc. 9th Int. Conf on Protocol Specification Testing and Verification INWG IFIP,
Ed. C. Vissers and E. Brinksma, pp. 317-326, Twente Neth., June 1989.
[PDF] Digital Photography
G.J. Holzmann
American Photographer, Jan. 1989, (invited paper).

1988
[PDF] The Digital Darkroom
G.J. Holzmann
Proc. SCAN - Small Computers in the Arts Network Conference, Nov. 1988, (invited paper).
[PDF] An Improved Protocol Reachability Analysis Technique
G.J. Holzmann
Software Practice Experience, Vol. 18, No. 2, pp. 137-161, Feb. 1988.
[PDF] Building a 3D Scanner for $1.99
G.J. Holzmann
unpublished draft, Jan. 1988.

1987
[PDF] X.21 Analysis Revisited: the Micro Tracer
G.J. Holzmann
AT&T Bell Laboratories Technical Memorandum TM 11271-8710230-12, Oct. 1987.
(See also microtrace.)
[PDF] Exhaustive analysis of a mutual exclusion algorithm
G.J. Holzmann
AT&T Bell Laboratories Technical Memorandum TM 11271-870609-08, June 1987.
[PDF] On Limits and Possibilities of Automated Protocol Analysis
G.J. Holzmann
Proc. 6th Int. Conf on Protocol Specification Testing and Verification INWG IFIP,
Ed. H. Rudin and C. West, Zurich Switzerland, June 1987, (Invited paper).
[link] Pico - a picture editor
G.J. Holzmann
AT&T Technical Journal, Vol. 66, No. 2, pp. 2-13, Apr. 1987.
[PDF] Manual for the protocol analyzer Trace
G.J. Holzmann
AT&T Bell Laboratories, CSTR 134, Comp. Sci. Tech. Rep. Feb. 1987.

1986
[PDF] Protocol Tracing
G.J. Holzmann
Computer Networks and Simulation, Vol. III, North Holland Publ. Co, 1986.
[PDF] On the algebraic synthesis of protocols
G.J. Holzmann
AT&T Bell Labs Technical Memorandum, TM 11271-860609-04, June 1986.
[PDF] Automated protocol validation in Argos assertion proving and scatter searching
G.J. Holzmann
IEEE Transactions on Software Engineering, Vol. SE-13, No. 6, pp. 683-696, June 1986.

1985
[PDF] Trace: Performance Measurements
G.J. Holzmann
AT&T Bell Labs Technical Memorandum TM 850101-01, Jan. 1985.
[PDF] Tracing Protocols
G.J. Holzmann
AT&T Technical Journal, Vol. 64, No. 10, pp. 2413-2433, Dec. 1985.
(reprinted in: Current advances in distributed computation, Computer Science Press, 1986.)

1984
[PDF] The Unix Magician s Handbook - a review of The Unix Programming Environment
G.J. Holzmann
Unix: Login, 1984.
[PDF] Backward Symbolic Execution of Protocols
G.J. Holzmann
Proc. 4th Int. Conf on Protocol Specification Testing and Verification, INWG IFIP,
Ed. Y. Yemini, pp. 19-30, North Holland Publ. Co., Skytop PA USA, June 1984.
[PDF] The Pandora system - An Interactive System for the Design of Data Communication Protocols
G.J. Holzmann
Computer Networks, Vol. 8, No. 2, pp. 71-81, Apr. 1984.

1983
[PDF] Protocol Analysis on the PANDORA System: Four Examples
G.J. Holzmann
AVS Laboratory, Report #45, Delft University, Sept. 1983.
[jpg] Systeem Krakers - Spelen Met de Computer
G.J. Holzmann
NRC Handelsblad, Science Supplement, Sept. 1983, (in Dutch).
[PDF] The PANDORA Protocol Development System
G.J. Holzmann and R. A. Beukers
Proc. 3rd Int. Conf on Protocol Specification Testing and Verification, INWG IFIP,
Ed. H. Rudin and C. West, pp. 357-369, North Holland Publ., Zurich, Switzerland, June 1983.
[PDF] Communicatie Protocollen - ontwerp analyse en standaardisatie
G.J. Holzmann
Informatie, Vol. 25, 1, pp. 5-11, Jan. 1983, (in Dutch).

1982
[PDF] A Theory for Protocol Validation
G.J. Holzmann
IEEE Transactions on Computers, Vol. C-31, 8, pp. 730-738, Aug. 1982.
[PDF] Concise Description of a Protocol Validation Algebra
G.J. Holzmann
AVS Laboratory, Report #38, Delft University, June 1982.
[PDF] Algebraic Validation Methods - A Comparison of Three Techniques
G.J. Holzmann
Proc. 2nd Int. Conf on Protocol Specification Testing and Verification, INWG IFIP,
Ed. C. Sunshine, pp. 383-391, North-Holland Publ., Idyllwild, CA, May 1982.

1981
Coordinatie - een net van betrouwbare processors
G.J. Holzmann
De Ingenieur, Vol. 93, No. 43, Oct. 1981 (in Dutch).
[PDF]
(5.7Mb)
The Problem of the Leidsestraat - An Exercise in Process Coordination
G.J. Holzmann
AVS Laboratory, Report #36, Delft University, Aug. 1981.
An Algebra for Protocol Validation
G.J. Holzmann
Proc. 1st Int. Conf on Protocol Specification Testing and Verification, INWG IFIP,
Ed. C. Sunshine and D. Rayner, pp. 377-391, England, May 1981.
[PDF] PAN - A Protocol Specification Analyzer
G.J. Holzmann
AT&T Bell Laboratories, Technical Memorandum TM81-11271-5, 1981.

1980
[PDF]
(7.6Mb)
The Design of Coordination Schemes
G.J. Holzmann
Proc. USC ISI Workshop on Concurrency, Idyllwild Calif., Mar. 1980.
AT&T Bell Laboratories, CSTR 87, Comp. Sci. Tech. Report, Aug. 1980.

1979
[link] Coordination Problems in Multiprocessing Systems
G.J. Holzmann
Ph.D. Thesis, Delft University Press, Delft, The Netherlands, June 1979.

Return to home page.
Page last modified: 22 April 2023.