Algebraic Validation Methods-A Comparison of Three Techniques. - Gerard J. Holzmann (PSTV, 1982)

A Theory for Protocol Validation. - Gerard J. Holzmann (IEEE Trans. Computers, 1982)

The Pandora Protocol Development System. - Gerard J. Holzmann; Rob A. Beukers (Protocol Specification, Testing, and Verification, 1983)

Backward Symbolic Execution of Protocols. - Gerard J. Holzmann (PSTV, 1984)

The Pandora System: An Interactive System for the Design of Data Communication Protocols. - Gerard J. Holzmann (Comput. Networks, 1984)

Tracing protocols. - Gerard J. Holzmann (AT&T Tech. J., 1985)

On Limits and Possibilities of Automated Protocol Analysis. - Gerard J. Holzmann (PSTV, 1987)

Automated Protocol Validation in Argos: Assertion Proving and Scatter Searching. - Gerard J. Holzmann (IEEE Trans. Software Eng., 1987)

An Improved Protocol Reachability Analysis Technique. - Gerard J. Holzmann (Softw. Pract. Exp., 1988)

Validating SDL Specifications: an Experiment. - Gerard J. Holzmann; Joanna Patti (PSTV, 1989)

State-Space Caching Revisited. - Patrice Godefroid; Gerard J. Holzmann; Didier Pirottin (CAV, 1992)

Coverage Preserving Reduction Strategies for Reachability Analysis. - Gerard J. Holzmann; Patrice Godefroid; Didier Pirottin (PSTV, 1992)

Practical methods for the formal validation of SDL specifications. - Gerard J. Holzmann (Comput. Commun., 1992)

Protocol Design: Redefining the State of the Art. - Gerard J. Holzmann (IEEE Softw., 1992)

On the Verification of Temporal Properties. - Patrice Godefroid; Gerard J. Holzmann (PSTV, 1993)

Design and Validation of Protocols: A Tutorial. - Gerard J. Holzmann (Comput. Networks ISDN Syst., 1993)

Standardized Protocol Interfaces. - Gerard J. Holzmann (Softw. Pract. Exp., 1993)

Proving the value of formal methods. - Gerard J. Holzmann (FORTE, 1994)

An improvement in formal verification. - Gerard J. Holzmann; Doron A. Peled (FORTE, 1994)

The Theory and Practice of A Formal Method: NewCoRe. - Gerard J. Holzmann (IFIP Congress (1), 1994)

Data Communications: The First 2500 Years. - Gerard J. Holzmann (IFIP Congress (2), 1994)

The early history of data networks. - Gerard J. Holzmann; Björn Pehrson (IEEE, 1995)

Tutorial: Proving Properties of Concurrent System with SPIN. - Gerard J. Holzmann (CONCUR, 1995)

An analysis of bistate hashing. - Gerard J. Holzmann (PSTV, 1995)

The State of SPIN. - Gerard J. Holzmann; Doron A. Peled (CAV, 1996)

Preface. - Jean-Charles Grégoire; Gerard J. Holzmann; Doron A. Peled (The Spin Verification System, 1996)

Not checking for closure under stuttering. - Gerard J. Holzmann; Orna Kupferman (The Spin Verification System, 1996)

On nested depth first search. - Gerard J. Holzmann; Doron A. Peled; Mihalis Yannakakis (The Spin Verification System, 1996)

Outline for an operational semantics of Promela. - V. Natarajan; Gerard J. Holzmann (The Spin Verification System, 1996)

Formal Methods for Early Fault Detection. - Gerard J. Holzmann (FTRTFT, 1996)

An Analyser for Mesage Sequence Charts. - Rajeev Alur; Gerard J. Holzmann; Doron A. Peled (TACAS, 1996)

Early Fault Detection Tools. - Gerard J. Holzmann (TACAS, 1996)

Formal Methods after 15 Years: Status and Trends (Paper based on contributions of the panelists at the FORmal TEchnique '95, Conference, Montreal, October 1995). - Jean-Pierre Courtiat; Piotr Dembinski; Gerard J. Holzmann; Luigi Logrippo; Harry Rudin; Pamela Zave (Comput. Networks ISDN Syst., 1996)

On-The-Fly Model Checking. - Gerard J. Holzmann (ACM Comput. Surv., 1996)

An Analyzer for Message Sequence Charts. - Rajeev Alur; Gerard J. Holzmann; Doron A. Peled (Softw. Concepts Tools, 1996)

Design tools for requirements engineering. - Gerard J. Holzmann; Doron A. Peled; Margaret H. Redberg (Bell Labs Tech. J., 1997)

Designing bug-free protocols with SPIN. - Gerard J. Holzmann (Comput. Commun., 1997)

The Model Checker SPIN. - Gerard J. Holzmann (IEEE Trans. Software Eng., 1997)

On Checking Model Checkers. - Gerard J. Holzmann (CAV, 1998)

Designing executable abstractions. - Gerard J. Holzmann (FMSP, 1998)

Validating Requirements for Fault Tolerant Systems using Model Checking. - Francis Schneider; Steve M. Easterbrook; John R. Callahan; Gerard J. Holzmann (ICRE, 1998)

Implementing Statecharts in PROMELA/SPIN. - Erich Mikk; Yassine Lakhnech; Michael Siegel; Gerard J. Holzmann (WIFT, 1998)

Interval reduction through requirements analysis. - Gerard J. Holzmann; Margaret H. Smith (Bell Labs Tech. J., 1998)

An Analysis of Bitstate Hashing. - Gerard J. Holzmann (Formal Methods Syst. Des., 1998)

Software Model Checking. - Gerard J. Holzmann; Margaret H. Smith (FORTE, 1999)

A Practical Method for Verifying Event-Driven Software. - Gerard J. Holzmann; Margaret H. Smith (ICSE, 1999)

v-Promela: A Visual, Object-Oriented Language for SPIN. - Stefan Leue; Gerard J. Holzmann (ISORC, 1999)

The Engineering of a Model Checker: The Gnu i-Protocol Case Study Revisited. - Gerard J. Holzmann (SPIN, 1999)

A Minimized Automaton Representation of Reachable States. - Gerard J. Holzmann; Anuj Puri (Int. J. Softw. Tools Technol. Transf., 1999)

Optimizing Büchi Automata. - Kousha Etessami; Gerard J. Holzmann (CONCUR, 2000)

Logic Verification of ANSI-C Code with SPIN. - Gerard J. Holzmann (SPIN, 2000)

Software verification at Bell Labs: One line of development. - Gerard J. Holzmann (Bell Labs Tech. J., 2000)

Automating software feature verification. - Gerard J. Holzmann; Margaret H. Smith (Bell Labs Tech. J., 2000)

SPIN Model Checking: An Introduction. - Gerard J. Holzmann; Elie Najm; Ahmed Serhrouchni (Int. J. Softw. Tools Technol. Transf., 2000)

From Code to Models. - Gerard J. Holzmann (ACSD, 2001)

Economics of software verification. - Gerard J. Holzmann (PASTE, 2001)

Events and Constraints: A Graphical Editor for Capturing Logic Requirements of Programs. - Margaret H. Smith; Gerard J. Holzmann; Kousha Etessami (RE, 2001)

Software model checking: extracting verification models from source code. - Gerard J. Holzmann; Margaret H. Smith (Softw. Test. Verification Reliab., 2001)

Abstracting C with abC. - Dennis Dams; William Hesse; Gerard J. Holzmann (CAV, 2002)

Software Analysis and Model Checking. - Gerard J. Holzmann (CAV, 2002)

The logic of bugs. - Gerard J. Holzmann (SIGSOFT FSE, 2002)

An Automated Verification Method for Distributed Systems Software Based on Model Extraction. - Gerard J. Holzmann; Margaret H. Smith (IEEE Trans. Software Eng., 2002)

Trends in Software Verification. - Gerard J. Holzmann (FME, 2003)

Fighting livelock in the GNU i-protocol: a case study in explicit-state model checking. - Yifei Dong; Xiaoqun Du; Gerard J. Holzmann; Scott A. Smolka (Int. J. Softw. Tools Technol. Transf., 2003)

The SPIN Model Checker - primer and reference manual. - Gerard J. Holzmann (Addison-Wesley, 2004)

Formal methods and software reliability. - Gerard J. Holzmann (MEMOCODE, 2004)

Model-Driven Software Verification. - Gerard J. Holzmann; Rajeev Joshi (SPIN, 2004)

Advanced SPIN Tutorial. - Theo C. Ruys; Gerard J. Holzmann (SPIN, 2004)

Improving Spin's Partial-Order Reduction for Breadth-First Search. - Dragan Bosnacki; Gerard J. Holzmann (SPIN, 2005)

Effective Bug Hunting with Spin and Modex. - Gerard J. Holzmann; Theo C. Ruys (SPIN, 2005)

Reliable Software Systems Design: Defect Prevention, Detection, and Containment. - Gerard J. Holzmann; Rajeev Joshi (VSTTE, 2005)

A Mini Challenge: Build a Verifiable Filesystem. - Rajeev Joshi; Gerard J. Holzmann (VSTTE, 2005)

Software model checking with SPIN. - Gerard J. Holzmann (Adv. Comput., 2005)

The Power of 10: Rules for Developing Safety-Critical Code. - Gerard J. Holzmann (Computer, 2006)

Randomized Differential Testing as a Prelude to Formal Verification. - Alex Groce; Gerard J. Holzmann; Rajeev Joshi (ICSE, 2007)

Multi-Core Model Checking with SPIN. - Gerard J. Holzmann; Dragan Bosnacki (IPDPS, 2007)

Conquering Complexity. - Gerard J. Holzmann (Computer, 2007)

A Stack-Slicing Algorithm for Multi-Core Model Checking. - Gerard J. Holzmann (PDMC@CAV, 2007)

The Design of a Multicore Extension of the SPIN Model Checker. - Gerard J. Holzmann; Dragan Bosnacki (IEEE Trans. Software Eng., 2007)

Swarm Verification. - Gerard J. Holzmann; Rajeev Joshi; Alex Groce (ASE, 2008)

Automated Testing of Planning Models. - Klaus Havelund; Alex Groce; Gerard J. Holzmann; Rajeev Joshi; Margaret H. Smith (MoChArt, 2008)

Tackling Large Verification Problems with the Swarm Tool. - Gerard J. Holzmann; Rajeev Joshi; Alex Groce (SPIN, 2008)

New Challenges in Model Checking. - Gerard J. Holzmann; Rajeev Joshi; Alex Groce (25 Years of Model Checking, 2008)

Model driven code checking. - Gerard J. Holzmann; Rajeev Joshi; Alex Groce (Autom. Softw. Eng., 2008)

Software Safety and Rocket Science. - Gerard J. Holzmann (ERCIM News, 2008)

Formal Software Verification: How Close Are We? - Gerard J. Holzmann (FMOODS/FORTE, 2010)

SCRUB: a tool for code reviews. - Gerard J. Holzmann (Innov. Syst. Softw. Eng., 2010)

Software certification: coding, code, and coders. - Klaus Havelund; Gerard J. Holzmann (EMSOFT, 2011)

Model Checking Multitask Applications for OSEK Compliant Real-Time Operating Systems. - Mark L. McKelvin Jr.; Edward B. Gamble Jr.; Gerard J. Holzmann (PRDC, 2011)

Reliable Software Development: Analysis-Aware Design. - Gerard J. Holzmann (TACAS, 2011)

Model checking with bounded context switching. - Gerard J. Holzmann; Mihai Florian (Formal Aspects Comput., 2011)

Swarm Verification Techniques. - Gerard J. Holzmann; Rajeev Joshi; Alex Groce (IEEE Trans. Software Eng., 2011)

Conquering Complexity. - Gerard J. Holzmann (Conquering Complexity, 2012)

Logic Model Checking of Time-Periodic Real-Time Systems. - Mihai Florian; Edward B. Gamble; Gerard J. Holzmann (Infotech@Aerospace, 2012)

Parallelizing the Spin Model Checker. - Gerard J. Holzmann (SPIN, 2012)

Keynote speaker 1: The economics of systems and software reliability. - Barry W. Boehm; Gerard J. Holzmann (ISSRE, 2013)

Proving Properties of Concurrent Programs - (Extended Abstract). - Gerard J. Holzmann (SPIN, 2013)

A Three-Step Program for Recovering Hackers. - Gerard J. Holzmann (Computer, 2013)

Landing a Spacecraft on Mars. - Gerard J. Holzmann (IEEE Softw., 2013)

An improvement of the piggyback algorithm for parallel model checking. - Ioannis Filippidis; Gerard J. Holzmann (SPIN, 2014)

Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning. - Alex Groce; Klaus Havelund; Gerard J. Holzmann; Rajeev Joshi; Ru-Gang Xu (Ann. Math. Artif. Intell., 2014)

Mars code. - Gerard J. Holzmann (Commun. ACM, 2014)

Fault Intolerance [Reliable Code]. - Gerard J. Holzmann (IEEE Softw., 2014)

A multi-paradigm language for reactive synthesis. - Ioannis Filippidis; Richard M. Murray; Gerard J. Holzmann (SYNT, 2015)

To Code Is Human. - Gerard J. Holzmann (IEEE Softw., 2015)

Code Inflation. - Gerard J. Holzmann (IEEE Softw., 2015)

Assertive Testing. - Gerard J. Holzmann (IEEE Softw., 2015)

Points of Truth. - Gerard J. Holzmann (IEEE Softw., 2015)

Code Evasion. - Gerard J. Holzmann (IEEE Softw., 2015)

Out of Bounds. - Gerard J. Holzmann (IEEE Softw., 2015)

Cloud-Based Verification of Concurrent Software. - Gerard J. Holzmann (VMCAI, 2016)

Tiny Tools. - Gerard J. Holzmann (IEEE Softw., 2016)

Code Clarity. - Gerard J. Holzmann (IEEE Softw., 2016)

Frequently Unanswered Questions. - Gerard J. Holzmann (IEEE Softw., 2016)

The Weakest Link. - Gerard J. Holzmann (IEEE Softw., 2016)

Brace Yourself. - Gerard J. Holzmann (IEEE Softw., 2016)

Hi Maintenance. - Gerard J. Holzmann (IEEE Softw., 2016)

Cobra - an interactive static code analyzer. - Gerard J. Holzmann (ASE, 2017)

Cobra: fast structural code checking (keynote). - Gerard J. Holzmann (SPIN, 2017)

Cobra: a light-weight tool for static and dynamic program analysis. - Gerard J. Holzmann (Innov. Syst. Softw. Eng., 2017)

The Value of Doubt. - Gerard J. Holzmann (IEEE Softw., 2017)

Code Craft. - Gerard J. Holzmann (IEEE Softw., 2017)

A Tale of Three Programs. - Gerard J. Holzmann (IEEE Softw., 2017)

Dead Programs. - Gerard J. Holzmann (IEEE Softw., 2017)

Randomly Right. - Gerard J. Holzmann (IEEE Softw., 2017)

Ends and Means. - Gerard J. Holzmann (IEEE Softw., 2018)

Curve Balls. - Gerard J. Holzmann (IEEE Softw., 2018)

Software Components. - Gerard J. Holzmann (IEEE Softw., 2018)

Code Vault. - Gerard J. Holzmann (IEEE Softw., 2018)

Explicit-State Model Checking. - Gerard J. Holzmann (Handbook of Model Checking, 2018)

Formalizing Requirements Is Diamond Box Hard. - Gerard J. Holzmann (From Reactive Systems to Cyber-Physical Systems, 2019)

Code Mining. - Gerard J. Holzmann (IEEE Softw., 2019)

Does Not Compute. - Gerard J. Holzmann (IEEE Softw., 2019)

Code Overload. - Gerard J. Holzmann (IEEE Softw., 2019)

Predicting the Past. - Gerard J. Holzmann (IEEE Softw., 2020)

Test Fatigue. - Gerard J. Holzmann (IEEE Softw., 2020)

Comparing Two Methods for Checking Runtime Properties. - Gerard J. Holzmann (Formal Methods in Outer Space, 2021)

Model-Checking Support for File System Development. - Wei Su; Yifei Liu; Gomathi Ganesan; Gerard J. Holzmann; Scott A. Smolka; Erez Zadok; Geoff Kuenning (HotStorage, 2021)

Interactive analysis of large code bases (invited talk). - Gerard J. Holzmann (ESEC/SIGSOFT FSE, 2021)

Right Code. - Gerard J. Holzmann (IEEE Softw., 2021)

Keeping It Simple: Agile Analysis. - Gerard J. Holzmann (IEEE Softw., 2021)

Metis: File System Model Checking via Versatile Input and State Exploration. - Yifei Liu; Manish Adkar; Gerard J. Holzmann; Geoff Kuenning; Pei Liu; Scott A. Smolka; Wei Su; Erez Zadok (FAST, 2024)

Artifact Package: the Metis File System Model Checking Framework. - Yifei Liu; Manish Adkar; Gerard J. Holzmann; Geoff Kuenning; Pei Liu; Scott A. Smolka; Wei Su; Erez Zadok (Zenodo, 2024)

Artifact Package: the RefFS Reference File System for the Metis Model Checking Framework. - Yifei Liu; Manish Adkar; Gerard J. Holzmann; Geoff Kuenning; Pei Liu; Scott A. Smolka; Wei Su; Erez Zadok (Zenodo, 2024)

Programming event monitors. - Klaus Havelund; Gerard J. Holzmann (Int. J. Softw. Tools Technol. Transf., 2024)