Gerard J. Holzmann

Proceedings of the Formal Methods in Outer Space, 2021

2020

Test Fatigue.

[BibT_eX]

[DOI]

IEEE Softw., 2020

Predicting the Past.

[BibT_eX]

[DOI]

IEEE Softw., 2020

2019

Code Overload.

[BibT_eX]

[DOI]

IEEE Softw., 2019

Does Not Compute.

[BibT_eX]

[DOI]

IEEE Softw., 2019

Code Mining.

[BibT_eX]

[DOI]

IEEE Softw., 2019

Formalizing Requirements Is \Diamond \Box Hard.

[BibT_eX]

[DOI]

Proceedings of the From Reactive Systems to Cyber-Physical Systems, 2019

2018

Explicit-State Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Handbook of Model Checking., 2018

Code Vault.

[BibT_eX]

[DOI]

IEEE Softw., 2018

Software Components.

[BibT_eX]

[DOI]

IEEE Softw., 2018

Curve Balls.

[BibT_eX]

[DOI]

IEEE Softw., 2018

Ends and Means.

[BibT_eX]

[DOI]

IEEE Softw., 2018

2017

Randomly Right.

[BibT_eX]

[DOI]

IEEE Softw., 2017

Dead Programs.

[BibT_eX]

[DOI]

IEEE Softw., 2017

A Tale of Three Programs.

[BibT_eX]

[DOI]

IEEE Softw., 2017

Code Craft.

[BibT_eX]

[DOI]

IEEE Softw., 2017

The Value of Doubt.

[BibT_eX]

[DOI]

IEEE Softw., 2017

Cobra: a light-weight tool for static and dynamic program analysis.

[BibT_eX]

[DOI]

Innov. Syst. Softw. Eng., 2017

Cobra: fast structural code checking (keynote).

[BibT_eX]

[DOI]

Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, 2017

Cobra - an interactive static code analyzer.

[BibT_eX]

[DOI]

Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering, 2017

2016

Hi Maintenance.

[BibT_eX]

[DOI]

IEEE Softw., 2016

Brace Yourself.

[BibT_eX]

[DOI]

IEEE Softw., 2016

The Weakest Link.

[BibT_eX]

[DOI]

IEEE Softw., 2016

Frequently Unanswered Questions.

[BibT_eX]

[DOI]

IEEE Softw., 2016

Code Clarity.

[BibT_eX]

[DOI]

IEEE Softw., 2016

Tiny Tools.

[BibT_eX]

[DOI]

IEEE Softw., 2016

Cloud-Based Verification of Concurrent Software.

[BibT_eX]

[DOI]

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2016

2015

Out of Bounds.

[BibT_eX]

[DOI]

IEEE Softw., 2015

Code Evasion.

[BibT_eX]

[DOI]

IEEE Softw., 2015

Points of Truth.

[BibT_eX]

[DOI]

IEEE Softw., 2015

Assertive Testing.

[BibT_eX]

[DOI]

IEEE Softw., 2015

Code Inflation.

[BibT_eX]

[DOI]

IEEE Softw., 2015

To Code Is Human.

[BibT_eX]

[DOI]

IEEE Softw., 2015

A multi-paradigm language for reactive synthesis.

[BibT_eX]

[DOI]

Ioannis Filippidis

Richard M. Murray

Proceedings of the Proceedings Fourth Workshop on Synthesis, 2015

2014

Fault Intolerance [Reliable Code].

[BibT_eX]

[DOI]

IEEE Softw., 2014

Mars code.

[BibT_eX]

[DOI]

Commun. ACM, 2014

Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning.

[BibT_eX]

[DOI]

Ann. Math. Artif. Intell., 2014

An improvement of the piggyback algorithm for parallel model checking.

[BibT_eX]

[DOI]

Ioannis Filippidis

Proceedings of the 2014 International Symposium on Model Checking of Software, 2014

2013

Landing a Spacecraft on Mars.

[BibT_eX]

[DOI]

IEEE Softw., 2013

A Three-Step Program for Recovering Hackers.

[BibT_eX]

[DOI]

Computer, 2013

Proving Properties of Concurrent Programs - (Extended Abstract).

[BibT_eX]

[DOI]

Proceedings of the Model Checking Software - 20th International Symposium, 2013

Keynote speaker 1: The economics of systems and software reliability.

[BibT_eX]

[DOI]

Barry W. Boehm

Proceedings of the IEEE 24th International Symposium on Software Reliability Engineering, 2013

2012

Parallelizing the Spin Model Checker.

[BibT_eX]

[DOI]

Proceedings of the Model Checking Software - 19th International Workshop, 2012

Logic Model Checking of Time-Periodic Real-Time Systems.

[BibT_eX]

[DOI]

Mihai Florian

Edward B. Gamble

Proceedings of the Infotech@Aerospace 2012, 2012

Conquering Complexity.

[BibT_eX]

[DOI]

Proceedings of the Conquering Complexity, 2012

2011

Swarm Verification Techniques.

[BibT_eX]

[DOI]

IEEE Trans. Software Eng., 2011

Model checking with bounded context switching.

[BibT_eX]

[DOI]

Mihai Florian

Formal Aspects Comput., 2011

Reliable Software Development: Analysis-Aware Design.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2011

Model Checking Multitask Applications for OSEK Compliant Real-Time Operating Systems.

[BibT_eX]

[DOI]

Mark L. McKelvin Jr.

Edward B. Gamble Jr.

Proceedings of the 17th IEEE Pacific Rim International Symposium on Dependable Computing, 2011

Software certification: coding, code, and coders.

[BibT_eX]

[DOI]

Klaus Havelund

Proceedings of the 11th International Conference on Embedded Software, 2011

2010

SCRUB: a tool for code reviews.

[BibT_eX]

[DOI]

Innov. Syst. Softw. Eng., 2010

Formal Software Verification: How Close Are We?

[BibT_eX]

[DOI]

Proceedings of the Formal Techniques for Distributed Systems, 2010

2008

Software Safety and Rocket Science.

[BibT_eX]

[DOI]

ERCIM News, 2008

Model driven code checking.

[BibT_eX]

[DOI]

Autom. Softw. Eng., 2008

New Challenges in Model Checking.

[BibT_eX]

[DOI]

Proceedings of the 25 Years of Model Checking - History, Achievements, Perspectives, 2008

Tackling Large Verification Problems with the Swarm Tool.

[BibT_eX]

[DOI]

Proceedings of the Model Checking Software, 2008

Automated Testing of Planning Models.

[BibT_eX]

[DOI]

Proceedings of the Model Checking and Artificial Intelligence, 5th International Workshop, 2008

Swarm Verification.

[BibT_eX]

[DOI]

Proceedings of the 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE 2008), 2008

2007

The Design of a Multicore Extension of the SPIN Model Checker.

[BibT_eX]

[DOI]

Dragan Bosnacki

IEEE Trans. Software Eng., 2007

A mini challenge: build a verifiable filesystem.

[BibT_eX]

[DOI]

Formal Aspects Comput., 2007

A Stack-Slicing Algorithm for Multi-Core Model Checking.

[BibT_eX]

[DOI]

Proceedings of the 6th International Workshop on Parallel and Distributed Methods in verifiCation, 2007

Conquering Complexity.

[BibT_eX]

[DOI]

Computer, 2007

Multi-Core Model Checking with SPIN.

[BibT_eX]

[DOI]

Dragan Bosnacki

Proceedings of the 21th International Parallel and Distributed Processing Symposium (IPDPS 2007), 2007

Randomized Differential Testing as a Prelude to Formal Verification.

[BibT_eX]

[DOI]

Proceedings of the 29th International Conference on Software Engineering (ICSE 2007), 2007

2006

The Power of 10: Rules for Developing Safety-Critical Code.

[BibT_eX]

[DOI]

Computer, 2006

2005

Software model checking with SPIN.

[BibT_eX]

[DOI]

Adv. Comput., 2005

Reliable Software Systems Design: Defect Prevention, Detection, and Containment.

[BibT_eX]

[DOI]

Proceedings of the Verified Software: Theories, 2005

Effective Bug Hunting with Spin and Modex.

[BibT_eX]

[DOI]

Theo C. Ruys

Proceedings of the Model Checking Software, 2005

Improving Spin's Partial-Order Reduction for Breadth-First Search.

[BibT_eX]

[DOI]

Dragan Bosnacki

Proceedings of the Model Checking Software, 2005

2004

Advanced SPIN Tutorial.

[BibT_eX]

[DOI]

Theo C. Ruys

Proceedings of the Model Checking Software, 2004

Model-Driven Software Verification.

[BibT_eX]

[DOI]

Proceedings of the Model Checking Software, 2004

Formal methods and software reliability.

[BibT_eX]

[DOI]

Proceedings of the 2nd ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2004), 2004

The SPIN Model Checker - primer and reference manual.

[BibT_eX]

Addison-Wesley, ISBN: 978-0-321-22862-8, 2004

2003

Fighting livelock in the GNU i-protocol: a case study in explicit-state model checking.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2003

Trends in Software Verification.

[BibT_eX]

[DOI]

Proceedings of the FME 2003: Formal Methods, 2003

2002

An Automated Verification Method for Distributed Systems Software Based on Model Extraction.

[BibT_eX]

[DOI]

IEEE Trans. Software Eng., 2002

The logic of bugs.

[BibT_eX]

[DOI]

Proceedings of the Tenth ACM SIGSOFT Symposium on Foundations of Software Engineering 2002, 2002

Software Analysis and Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 14th International Conference, 2002

Abstracting C with abC.

[BibT_eX]

[DOI]

Dennis Dams

William Hesse

Proceedings of the Computer Aided Verification, 14th International Conference, 2002

2001

Software model checking: extracting verification models from source code.

[BibT_eX]

Softw. Test. Verification Reliab., 2001

Events and Constraints: A Graphical Editor for Capturing Logic Requirements of Programs.

[BibT_eX]

[DOI]

Kousha Etessami

Proceedings of the 5th IEEE International Symposium on Requirements Engineering (RE 2001), 2001

Economics of software verification.

[BibT_eX]

[DOI]

Proceedings of the 2001 ACM SIGPLAN-SIGSOFT Workshop on Program Analysis For Software Tools and Engineering, 2001

From Code to Models.

[BibT_eX]

[DOI]

Proceedings of the 2nd International Conference on Application of Concurrency to System Design (ACSD 2001), 2001

2000

SPIN Model Checking: An Introduction.

[BibT_eX]

[DOI]

Elie Najm

Ahmed Serhrouchni

Int. J. Softw. Tools Technol. Transf., 2000

Automating software feature verification.

[BibT_eX]

[DOI]

Bell Labs Tech. J., 2000

Software verification at Bell Labs: One line of development.

[BibT_eX]

[DOI]

Bell Labs Tech. J., 2000

Logic Verification of ANSI-C Code with SPIN.

[BibT_eX]

[DOI]

Proceedings of the SPIN Model Checking and Software Verification, 7th International SPIN Workshop, Stanford, CA, USA, August 30, 2000

Optimizing Büchi Automata.

[BibT_eX]

[DOI]

Kousha Etessami

Proceedings of the CONCUR 2000, 2000

1999

A Minimized Automaton Representation of Reachable States.

[BibT_eX]

[DOI]

Anuj Puri

Int. J. Softw. Tools Technol. Transf., 1999

The Engineering of a Model Checker: The Gnu i-Protocol Case Study Revisited.

[BibT_eX]

[DOI]

Proceedings of the Theoretical and Practical Aspects of SPIN Model Checking, 1999

v-Promela: A Visual, Object-Oriented Language for SPIN.

[BibT_eX]

[DOI]

Stefan Leue

Proceedings of the 2nd International Symposium on Object-Oriented Real-Time Distributed Computing (ISORC '99), 1999

A Practical Method for Verifying Event-Driven Software.

[BibT_eX]

[DOI]

Proceedings of the 1999 International Conference on Software Engineering, 1999

Software Model Checking.

[BibT_eX]

Proceedings of the Formal Methods for Protocol Engineering and Distributed Systems, 1999

1998

An Analysis of Bitstate Hashing.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 1998

Interval reduction through requirements analysis.

[BibT_eX]

[DOI]

Bell Labs Tech. J., 1998

Implementing Statecharts in PROMELA/SPIN.

[BibT_eX]

[DOI]

Proceedings of the 2nd Workshop on Industrial-Strength Formal Specification Techniques (WIFT '98), 1998

Validating Requirements for Fault Tolerant Systems using Model Checking.

[BibT_eX]

[DOI]

Proceedings of the 3rd International Conference on Requirements Engineering (ICRE '98), 1998

Designing executable abstractions.

[BibT_eX]

[DOI]

Proceedings of the Second Workshop on Formal Methods in Software Practice, 1998

On Checking Model Checkers.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 10th International Conference, 1998

1997

The Model Checker SPIN.

[BibT_eX]

[DOI]

IEEE Trans. Software Eng., 1997

Designing bug-free protocols with SPIN.

[BibT_eX]

[DOI]

Comput. Commun., 1997

Design tools for requirements engineering.

[BibT_eX]

[DOI]

Margaret H. Redberg

Bell Labs Tech. J., 1997

1996

Early Fault Detection Tools.

[BibT_eX]

Softw. Concepts Tools, 1996

An Analyzer for Message Sequence Charts.

[BibT_eX]

Rajeev Alur

Softw. Concepts Tools, 1996

On-The-Fly Model Checking.

[BibT_eX]

[DOI]

ACM Comput. Surv., 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).

[BibT_eX]

[DOI]

Comput. Networks ISDN Syst., 1996

An Analyser for Mesage Sequence Charts.

[BibT_eX]

[DOI]

Rajeev Alur

Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 1996

Formal Methods for Early Fault Detection.

[BibT_eX]

[DOI]

Proceedings of the Formal Techniques in Real-Time and Fault-Tolerant Systems, 1996

Outline for an operational semantics of Promela.

[BibT_eX]

[DOI]

V. Natarajan

Proceedings of the Spin Verification System, 1996

On nested depth first search.

[BibT_eX]

[DOI]

Mihalis Yannakakis

Proceedings of the Spin Verification System, 1996

Not checking for closure under stuttering.

[BibT_eX]

[DOI]

Orna Kupferman

Proceedings of the Spin Verification System, 1996

Preface.

[BibT_eX]

Jean-Charles Grégoire

Proceedings of the Spin Verification System, 1996

The State of SPIN.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 8th International Conference, 1996

1995

State-Space Caching Revisited.

[BibT_eX]

[DOI]

Patrice Godefroid

Didier Pirottin

Formal Methods Syst. Des., 1995

An analysis of bistate hashing.

[BibT_eX]

Proceedings of the Protocol Specification, 1995

Tutorial: Proving Properties of Concurrent System with SPIN.

[BibT_eX]

[DOI]

Proceedings of the CONCUR '95: Concurrency Theory, 1995

The early history of data networks.

[BibT_eX]

Björn Pehrson

IEEE, ISBN: 978-0-8186-6782-4, 1995

1994

Data Communications: The First 2500 Years.

[BibT_eX]

Proceedings of the Applications and Impacts, Information Processing '94, Volume 2, Proceedings of the IFIP 13th World Computer Congress, Hamburg, Germany, 28 August, 1994

The Theory and Practice of A Formal Method: NewCoRe.

[BibT_eX]

Proceedings of the Technology and Foundations - Information Processing '94, Volume 1, Proceedings of the IFIP 13th World Computer Congress, Hamburg, Germany, 28 August, 1994

An improvement in formal verification.

[BibT_eX]

Proceedings of the Formal Description Techniques VII, 1994

Proving the value of formal methods.

[BibT_eX]

Proceedings of the Formal Description Techniques VII, 1994

1993

Standardized Protocol Interfaces.

[BibT_eX]

[DOI]

Softw. Pract. Exp., 1993

Design and Validation of Protocols: A Tutorial.

[BibT_eX]

[DOI]

Comput. Networks ISDN Syst., 1993

On the Verification of Temporal Properties.

[BibT_eX]

Patrice Godefroid

Proceedings of the Protocol Specification, 1993

1992

Protocol Design: Redefining the State of the Art.

[BibT_eX]

[DOI]

IEEE Softw., 1992

Practical methods for the formal validation of SDL specifications.

[BibT_eX]

[DOI]

Comput. Commun., 1992

Coverage Preserving Reduction Strategies for Reachability Analysis.

[BibT_eX]

Patrice Godefroid

Didier Pirottin

Proceedings of the Protocol Specification, 1992

1989

Validating SDL Specifications: an Experiment.

[BibT_eX]

Joanna Patti

Proceedings of the Protocol Specification, 1989

1988

An Improved Protocol Reachability Analysis Technique.

[BibT_eX]

[DOI]

Softw. Pract. Exp., 1988

1987

Automated Protocol Validation in <i>Argos: </i> Assertion Proving and Scatter Searching.

[BibT_eX]

[DOI]

IEEE Trans. Software Eng., 1987

On Limits and Possibilities of Automated Protocol Analysis.

[BibT_eX]

Proceedings of the Protocol Specification, 1987

1985

Tracing protocols.

[BibT_eX]

[DOI]

AT&T Tech. J., 1985

1984

The Pandora System: An Interactive System for the Design of Data Communication Protocols.

[BibT_eX]

[DOI]

Comput. Networks, 1984

Backward Symbolic Execution of Protocols.

[BibT_eX]

Proceedings of the Protocol Specification, 1984

1983

The Pandora Protocol Development System.

[BibT_eX]

Rob A. Beukers

Proceedings of the Protocol Specification, Testing, and Verification, III, Proceedings of the IFIP WG 6.1 Third International Workshop on Protocol Specification, Testing and Verification, organized by IBM Research, Rüschlikon, Switzerland, 31 May, 1983

1982

A Theory for Protocol Validation.

[BibT_eX]

[DOI]

IEEE Trans. Computers, 1982

Algebraic Validation Methods-A Comparison of Three Techniques.

[BibT_eX]