We stand with Ukraine

We stand with Ukraine

John M. Rushby

According to our database¹, John M. Rushby authored at least 75 papers between 1981 and 2014.

Collaborative distances:

Dijkstra number² of three.
Erdős number³ of three.

Timeline

Legend:

Book

In proceedings

Article

PhD thesis

Dataset

Other

Links

On csauthors.net:

Bibliography

2014

Example of a Complementary Use of Model Checking and Human Performance Simulation.

[BibT_eX]

[DOI]

,

,

IEEE Trans. Hum. Mach. Syst., 2014

Safety envelope for security.

[BibT_eX]

[DOI]

,

,

Dejan Jovanovic

,

Thomas de Candia

,

Patrick Lincoln

,

,

,

Sanjit A. Seshia

Proceedings of the 3rd International Conference on High Confidence Networked Systems (part of CPS Week), 2014

2013

Example of a Complementary Use of Model Checking and Agent-Based Simulation.

[BibT_eX]

[DOI]

,

,

Proceedings of the IEEE International Conference on Systems, 2013

2012

The Versatile Synchronous Observer.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods: Foundations and Applications - 15th Brazilian Symposium, 2012

2011

Formal Modeling and Analysis for Interactive Hybrid Systems.

[BibT_eX]

[DOI]

,

,

,

Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2011

Toward a multi-method approach to formalizing human-automation interaction and human-human communications.

[BibT_eX]

[DOI]

,

Matthew L. Bolton

,

,

Dennis Griffith

,

,

,

Proceedings of the IEEE International Conference on Systems, 2011

New challenges in certification for aircraft software.

[BibT_eX]

[DOI]

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

Fractionated Software for Networked Cyber-Physical Systems: Research Directions and Long-Term Vision.

[BibT_eX]

[DOI]

Mark-Oliver Stehr

,

Carolyn L. Talcott

,

,

Patrick Lincoln

,

,

,

Proceedings of the Formal Modeling: Actors, Open Systems, Biological Systems, 2011

From DSS to MILS - (Extended Abstract).

[BibT_eX]

[DOI]

Proceedings of the Dependable and Historic Computing, 2011

2010

Formalism in Safety Cases.

[BibT_eX]

[DOI]

Proceedings of the Making Systems Safer, 2010

2009

Software Verification and System Assurance.

[BibT_eX]

[DOI]

Proceedings of the Seventh IEEE International Conference on Software Engineering and Formal Methods, 2009

2008

Runtime Certification.

[BibT_eX]

[DOI]

Proceedings of the Runtime Verification, 8th International Workshop, 2008

2007

An operational semantics for Stateflow.

[BibT_eX]

[DOI]

Grégoire Hamon

,

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

Automated Formal Methods Enter the Mainstream.

[BibT_eX]

[DOI]

J. Univers. Comput. Sci., 2007

What Use is Verified Software?

[BibT_eX]

[DOI]

Proceedings of the 12th International Conference on Engineering of Complex Computer Systems (ICECCS 2007), 2007

Just-in-Time Certification.

[BibT_eX]

[DOI]

Proceedings of the 12th International Conference on Engineering of Complex Computer Systems (ICECCS 2007), 2007

Distributed Secure Systems: Then and Now.

[BibT_eX]

[DOI]

,

Proceedings of the 23rd Annual Computer Security Applications Conference (ACSAC 2007), 2007

2006

PVS.

[BibT_eX]

[DOI]

,

Proceedings of the Seventeen Provers of the World, Foreword by Dana S. Scott, 2006

Tutorial: Automated Formal Methods with PVS, SAL, and Yices.

[BibT_eX]

[DOI]

Proceedings of the Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2006), 2006

Harnessing Disruptive Innovation in Formal Verification.

[BibT_eX]

[DOI]

Proceedings of the Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2006), 2006

Hybrid Systems - And Everything Else.

[BibT_eX]

[DOI]

Proceedings of the Hybrid Systems: Computation and Control, 9th International Workshop, 2006

2005

Automated Test Generation and Verified Software.

[BibT_eX]

[DOI]

Proceedings of the Verified Software: Theories, 2005

An Evidential Tool Bus.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2005

2004

Generating Efficient Test Sets with a Model Checker.

[BibT_eX]

[DOI]

Grégoire Hamon

,

Leonardo Mendonça de Moura

,

Proceedings of the 2nd International Conference on Software Engineering and Formal Methods (SEFM 2004), 2004

Model Checking a Fault-Tolerant Startup Algorithm: From Design Exploration To Exhaustive Fault Simulation.

[BibT_eX]

[DOI]

Wilfried Steiner

,

,

,

Proceedings of the 2004 International Conference on Dependable Systems and Networks (DSN 2004), 28 June, 2004

SAL 2.

[BibT_eX]

[DOI]

Leonardo Mendonça de Moura

,

,

,

,

Natarajan Shankar

,

,

Proceedings of the Computer Aided Verification, 16th International Conference, 2004

The ICS Decision Procedures for Embedded Deduction.

[BibT_eX]

[DOI]

Leonardo Mendonça de Moura

,

,

,

,

Natarajan Shankar

Proceedings of the Automated Reasoning - Second International Joint Conference, 2004

2003

Invisible formal methods for embedded control systems.

[BibT_eX]

[DOI]

,

Natarajan Shankar

,

Proc. IEEE, 2003

2002

Formally Verified Byzantine Agreement in Presence of Link Faults.

[BibT_eX]

[DOI]

,

,

Proceedings of the 22nd International Conference on Distributed Computing Systems (ICDCS'02), 2002

An Overview of Formal Verification for the Time-Triggered Architecture.

[BibT_eX]

[DOI]

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

2001

Modeling the Human in Human Factors.

[BibT_eX]

[DOI]

Proceedings of the Computer Safety, 2001

Bus Architectures for Safety-Critical Embedded Systems.

[BibT_eX]

[DOI]

Proceedings of the Embedded Software, First International Workshop, 2001

2000

Analyzing Cockpit Interfaces Using Formal Methods.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods Elsewhere, 2000

Theorem Proving for Verification.

[BibT_eX]

[DOI]

Proceedings of the Modeling and Verification of Parallel Processes, 4th Summer School, 2000

From Refutation to Verification.

[BibT_eX]

Proceedings of the Formal Techniques for Distributed System Development, 2000

Verification Diagrams Revisited: Disjunctive Invariants for Easy Verification.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 12th International Conference, 2000

1999

Systematic Formal Verification for Fault-Tolerant Time-Triggered Algorithms.

[BibT_eX]

[DOI]

IEEE Trans. Software Eng., 1999

A case-study in component-based mechanical verification of fault-tolerant programs.

[BibT_eX]

Sandeep S. Kulkarni

,

,

Natarajan Shankar

Proceedings of the 1999 ICDCS Workshop on Self-stabilizing Systems, 1999

Integrated Formal Verification: Using Model Checking with Automated Abstraction, Invariant Generation, and Theorem Proving.

[BibT_eX]

[DOI]

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

Mechanized Formal Methods: Where Next?

[BibT_eX]

[DOI]

Proceedings of the FM'99 - Formal Methods, 1999

Structural Embeddings: Mechanization with Method.

[BibT_eX]

[DOI]

César A. Muñoz

,

Proceedings of the FM'99 - Formal Methods, 1999

1998

Subtypes for Specifications: Predicate Subtyping in PVS.

[BibT_eX]

[DOI]

,

,

Natarajan Shankar

IEEE Trans. Software Eng., 1998

Ubiquitous Abstraction: A New Approach to Mechanized Formal Verification.

[BibT_eX]

[DOI]

Proceedings of the Second IEEE International Conference on Formal Engineering Methods, 1998

PVS: An Experience Report.

[BibT_eX]

[DOI]

,

,

Natarajan Shankar

,

David W. J. Stringer-Calvert

Proceedings of the Applied Formal Methods, 1998

1997

Low-Overhead Time-Triggered Group Membership.

[BibT_eX]

[DOI]

,

Patrick Lincoln

,

Proceedings of the Distributed Algorithms, 11th International Workshop, 1997

Integration in PVS: Tables, Types, and Model Checking.

[BibT_eX]

[DOI]

,

,

Natarajan Shankar

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

Calculating with Requirements.

[BibT_eX]

[DOI]

Proceedings of the 3rd IEEE International Symposium on Requirements Engineering (RE'97), 1997

Systematic Formal Verification of Interpreters.

[BibT_eX]

[DOI]

,

,

Mandayam K. Srivas

Proceedings of the First IEEE International Conference on Formal Engineering Methods, 1997

Subtypes for Specifications.

[BibT_eX]

[DOI]

Proceedings of the Software Engineering, 1997

1996

Enhancing the Utility of Formal Methods.

[BibT_eX]

[DOI]

ACM Comput. Surv., 1996

An Invitation to Formal Methods.

[BibT_eX]

[DOI]

Jonathan P. Bowen

,

Ricky W. Butler

,

,

Robert L. Glass

,

,

,

Michael G. Hinchey

,

C. Michael Holloway

,

,

,

Michael J. Lutz

,

David Lorge Parnas

,

,

Jeannette M. Wing

,

Computer, 1996

Reconfiguration and Transient Recovery in State Machine Architectures.

[BibT_eX]

[DOI]

Proceedings of the Digest of Papers: FTCS-26, 1996

Mechanized Formal Methods: Progress and Prospects.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1996

Automated Deduction and Formal Methods.

[BibT_eX]

[DOI]

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

PVS: Combining Specification, Proof Checking, and Model Checking.

[BibT_eX]

[DOI]

,

,

,

Natarajan Shankar

,

Mandayam K. Srivas

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

1995

Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS.

[BibT_eX]

[DOI]

,

,

Natarajan Shankar

,

Friedrich W. von Henke

IEEE Trans. Software Eng., 1995

Mechanizing Formal Methods: Opportunities and Challenges.

[BibT_eX]

[DOI]

Proceedings of the ZUM '95: The Z Formal Specification Notation, 1995

The Future of Formal Methods in Industry.

[BibT_eX]

[DOI]

,

David Lorge Parnas

,

,

,

Chris T. Sennett

Proceedings of the ZUM '95: The Z Formal Specification Notation, 1995

1994

A Tutorial on Using PVS for Hardware Verification.

[BibT_eX]

[DOI]

,

,

Natarajan Shankar

,

Mandayam K. Srivas

Proceedings of the Theorem Provers in Circuit Design, 1994

A Formally Verifiable Algorithm for Clock Synchronization under a Hybrid Fault Model.

[BibT_eX]

[DOI]

Proceedings of the Thirteenth Annual ACM Symposium on Principles of Distributed Computing, 1994

The PVS Verification System and PC/DC.

[BibT_eX]

,

Jens Ulrik Skakkebæk

Proceedings of the Formal Techniques in Real-Time and Fault-Tolerant Systems, Third International Symposium Organized Jointly with the Working Group Provably Correct Systems, 1994

1993

Formal Verification of Algorithms for Critical Systems.

[BibT_eX]

[DOI]

,

Friedrich W. von Henke

IEEE Trans. Software Eng., 1993

Using PVS to Prove Some Theorems Of David Parnas.

[BibT_eX]

[DOI]

,

Mandayam K. Srivas

Proceedings of the Higher Order Logic Theorem Proving and its Applications, 1993

A Formally Verified Algorithm for Interactive Consistency Under a Hybrid Fault Model.

[BibT_eX]

[DOI]

Patrick Lincoln

,

Proceedings of the Digest of Papers: FTCS-23, 1993

Limits in Dependability (Panel).

[BibT_eX]

[DOI]

Jean-Claude Laprie

,

Gérard Le Lann

,

Michele Morganti

,

Proceedings of the Digest of Papers: FTCS-23, 1993

Formal Verification for Fault-Tolerant Architectures: Some Lessons Learned.

[BibT_eX]

[DOI]

,

,

Natarajan Shankar

,

Friedrich W. von Henke

Proceedings of the FME '93: Industrial-Strength Formal Methods, 1993

The Formal Verification of an Algorithm for Interactive Consistency under a Hybrid Fault Model.

[BibT_eX]

[DOI]

Patrick Lincoln

,

Proceedings of the Computer Aided Verification, 5th International Conference, 1993

1992

Formal Specification and Verification of a Fault-Masking and Transient-Recovery Model for Digital Flight-Control Systems.

[BibT_eX]

[DOI]

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

PVS: A Prototype Verification System.

[BibT_eX]

[DOI]

,

,

Natarajan Shankar

Proceedings of the Automated Deduction, 1992

1991

Design Choices in Specification Languages and Verification Systems.

[BibT_eX]

Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, 1991

From formal verification to silicon compilation.

[BibT_eX]

[DOI]

,

,

,

Natarajan Shankar

,

,

Friedrich W. von Henke

Proceedings of the Compcon Spring '91, San Francisco, 1991

Model-Based Reconfiguration: Toward an Integration with Diagnosis.

[BibT_eX]

[DOI]

,

Proceedings of the 9th National Conference on Artificial Intelligence, 1991

1983

A Distributed Secure System.

[BibT_eX]

[DOI]

,

Computer, 1983

1982

Proof of separability: A verification technique for a class of a security kernels.

[BibT_eX]

[DOI]

Proceedings of the International Symposium on Programming, 1982

1981

Design and Verification of Secure Systems.

[BibT_eX]

[DOI]

Proceedings of the Eighth Symposium on Operating System Principles, 1981

Loading...