| 2007 |
|---|
| 61 | EE | Brian Randell,
John M. Rushby:
Distributed Secure Systems: Then and Now.
ACSAC 2007: 177-199 |
| 60 | EE | John M. Rushby:
Just-in-Time Certification.
ICECCS 2007: 15-24 |
| 59 | EE | John M. Rushby:
What Use is Verified Software?
ICECCS 2007: 270-276 |
| 58 | EE | Grégoire Hamon,
John M. Rushby:
An operational semantics for Stateflow.
STTT 9(5-6): 447-456 (2007) |
| 2006 |
|---|
| 57 | EE | John M. Rushby:
Hybrid Systems - And Everything Else.
HSCC 2006: 3 |
| 56 | EE | John M. Rushby:
Harnessing Disruptive Innovation in Formal Verification.
SEFM 2006: 21-30 |
| 55 | EE | John M. Rushby:
Tutorial: Automated Formal Methods with PVS, SAL, and Yices.
SEFM 2006: 262 |
| 54 | EE | Bart Jacobs,
John M. Rushby:
PVS.
The Seventeen Provers of the World 2006: 24-27 |
| 2005 |
|---|
| 53 | EE | John M. Rushby:
An Evidential Tool Bus.
ICFEM 2005: 36-36 |
| 2004 |
|---|
| 52 | EE | Leonardo Mendonça de Moura,
Sam Owre,
Harald Rueß,
John M. Rushby,
Natarajan Shankar,
Maria Sorea,
Ashish Tiwari:
SAL 2.
CAV 2004: 496-500 |
| 51 | EE | Wilfried Steiner,
John M. Rushby,
Maria Sorea,
Holger Pfeifer:
Model Checking a Fault-Tolerant Startup Algorithm: From Design Exploration To Exhaustive Fault Simulation.
DSN 2004: 189-198 |
| 50 | EE | Grégoire Hamon,
John M. Rushby:
An Operational Semantics for Stateflow.
FASE 2004: 229-243 |
| 49 | EE | Leonardo Mendonça de Moura,
Sam Owre,
Harald Rueß,
John M. Rushby,
Natarajan Shankar:
The ICS Decision Procedures for Embedded Deduction.
IJCAR 2004: 218-222 |
| 48 | EE | Grégoire Hamon,
Leonardo Mendonça de Moura,
John M. Rushby:
Generating Efficient Test Sets with a Model Checker.
SEFM 2004: 261-270 |
| 2003 |
|---|
| 47 | | Ashish Tiwari,
Natarajan Shankar,
John M. Rushby:
Invisible formal methods for embedded control systems.
Proceedings of the IEEE 91(1): 29-39 (2003) |
| 2002 |
|---|
| 46 | EE | John M. Rushby:
An Overview of Formal Verification for the Time-Triggered Architecture.
FTRTFT 2002: 83-106 |
| 45 | EE | Ulrich Schmid,
Bettina Weiss,
John M. Rushby:
Formally Verified Byzantine Agreement in Presence of Link Faults.
ICDCS 2002: 608-616 |
| 2001 |
|---|
| 44 | EE | John M. Rushby:
Bus Architectures for Safety-Critical Embedded Systems.
EMSOFT 2001: 306-323 |
| 43 | EE | John M. Rushby:
Modeling the Human in Human Factors.
SAFECOMP 2001: 86-91 |
| 42 | EE | John M. Rushby:
Analyzing Cockpit Interfaces Using Formal Methods.
Electr. Notes Theor. Comput. Sci. 43: (2001) |
| 2000 |
|---|
| 41 | | John M. Rushby:
Verification Diagrams Revisited: Disjunctive Invariants for Easy Verification.
CAV 2000: 508-520 |
| 40 | | John M. Rushby:
From Refutation to Verification.
FORTE 2000: 369-374 |
| 39 | EE | John M. Rushby:
Theorem Proving for Verification.
MOVEP 2000: 39-57 |
| 1999 |
|---|
| 38 | EE | John M. Rushby:
Integrated Formal Verification: Using Model Checking with Automated Abstraction, Invariant Generation, and Theorem Proving.
SPIN 1999: 1-11 |
| 37 | | Sandeep S. Kulkarni,
John M. Rushby,
Natarajan Shankar:
A case-study in component-based mechanical verification of fault-tolerant programs.
WSS 1999: 33-40 |
| 36 | EE | César Muñoz,
John M. Rushby:
Structural Embeddings: Mechanization with Method.
World Congress on Formal Methods 1999: 452-471 |
| 35 | EE | John M. Rushby:
Mechanized Formal Methods: Where Next?
World Congress on Formal Methods 1999: 48-51 |
| 34 | EE | John M. Rushby:
Systematic Formal Verification for Fault-Tolerant Time-Triggered Algorithms.
IEEE Trans. Software Eng. 25(5): 651-660 (1999) |
| 1998 |
|---|
| 33 | | Sam Owre,
John M. Rushby,
Natarajan Shankar,
David W. J. Stringer-Calvert:
PVS: An Experience Report.
FM-Trends 1998: 338-345 |
| 32 | EE | John M. Rushby:
Ubiquitous Abstraction: A New Approach to Mechanized Formal Verification.
ICFEM 1998: 176- |
| 31 | EE | John M. Rushby,
Sam Owre,
Natarajan Shankar:
Subtypes for Specifications: Predicate Subtyping in PVS.
IEEE Trans. Software Eng. 24(9): 709-720 (1998) |
| 1997 |
|---|
| 30 | EE | John M. Rushby:
Subtypes for Specifications.
ESEC / SIGSOFT FSE 1997: 4-19 |
| 29 | | David Cyrluk,
John M. Rushby,
Mandayam K. Srivas:
Systematic Formal Verification of Interpreters.
ICFEM 1997: 140- |
| 28 | | John M. Rushby:
Calculating with Requirements.
RE 1997: 144- |
| 27 | | Sam Owre,
John M. Rushby,
Natarajan Shankar:
Integration in PVS: Tables, Types, and Model Checking.
TACAS 1997: 366-383 |
| 26 | | Shmuel Katz,
Patrick Lincoln,
John M. Rushby:
Low-Overhead Time-Triggered Group Membership.
WDAG 1997: 155-169 |
| 1996 |
|---|
| 25 | | John M. Rushby:
Automated Deduction and Formal Methods.
CAV 1996: 169-183 |
| 24 | | Sam Owre,
S. Rajan,
John M. Rushby,
Natarajan Shankar,
Mandayam K. Srivas:
PVS: Combining Specification, Proof Checking, and Model Checking.
CAV 1996: 411-414 |
| 23 | | John M. Rushby:
Mechanized Formal Methods: Progress and Prospects.
FSTTCS 1996: 43-51 |
| 22 | | John M. Rushby:
Reconfiguration and Transient Recovery in State Machine Architectures.
FTCS 1996: 6-15 |
| 21 | | John M. Rushby:
Enhancing the Utility of Formal Methods.
ACM Comput. Surv. 28(4es): 123 (1996) |
| 20 | | Jonathan P. Bowen,
Ricky W. Butler,
David L. Dill,
Robert L. Glass,
David Gries,
Anthony Hall,
Michael G. Hinchey,
C. Michael Holloway,
Daniel Jackson,
Cliff B. Jones,
Michael J. Lutz,
David Lorge Parnas,
John M. Rushby,
Jeannette M. Wing,
Pamela Zave:
An Invitation to Formal Methods.
IEEE Computer 29(4): 16-30 (1996) |
| 1995 |
|---|
| 19 | | John M. Rushby:
Mechanizing Formal Methods: Opportunities and Challenges.
ZUM 1995: 105-113 |
| 18 | | Anthony Hall,
David Lorge Parnas,
Nico Plat,
John M. Rushby,
Chris T. Sennett:
The Future of Formal Methods in Industry.
ZUM 1995: 237-242 |
| 17 | EE | Sam Owre,
John M. Rushby,
Natarajan Shankar,
Friedrich W. von Henke:
Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS.
IEEE Trans. Software Eng. 21(2): 107-125 (1995) |
| 1994 |
|---|
| 16 | | John M. Rushby,
Jens Ulrik Skakkebæk:
The PVS Verification System and PC/DC.
FTRTFT 1994: 777-777 |
| 15 | | John M. Rushby:
A Formally Verifiable Algorithm for Clock Synchronization under a Hybrid Fault Model.
PODC 1994: 304-313 |
| 14 | | Sam Owre,
John M. Rushby,
Natarajan Shankar,
Mandayam K. Srivas:
A Tutorial on Using PVS for Hardware Verification.
TPCD 1994: 258-279 |
| 1993 |
|---|
| 13 | | Patrick Lincoln,
John M. Rushby:
The Formal Verification of an Algorithm for Interactive Consistency under a Hybrid Fault Model.
CAV 1993: 292-304 |
| 12 | | Sam Owre,
John M. Rushby,
Natarajan Shankar,
Friedrich W. von Henke:
Formal Verification for Fault-Tolerant Architectures: Some Lessons Learned.
FME 1993: 482-500 |
| 11 | | Patrick Lincoln,
John M. Rushby:
A Formally Verified Algorithm for Interactive Consistency Under a Hybrid Fault Model.
FTCS 1993: 402-411 |
| 10 | | Jean-Claude Laprie,
Gérard Le Lann,
Michele Morganti,
John M. Rushby:
Limits in Dependability (Panel).
FTCS 1993: 608-613 |
| 9 | | John M. Rushby,
Mandayam K. Srivas:
Using PVS to Prove Some Theorems Of David Parnas.
HUG 1993: 163-173 |
| 8 | EE | John M. Rushby,
Friedrich W. von Henke:
Formal Verification of Algorithms for Critical Systems.
IEEE Trans. Software Eng. 19(1): 13-23 (1993) |
| 1992 |
|---|
| 7 | | Sam Owre,
John M. Rushby,
Natarajan Shankar:
PVS: A Prototype Verification System.
CADE 1992: 748-752 |
| 6 | | John M. Rushby:
Formal Specification and Verification of a Fault-Masking and Transient-Recovery Model for Digital Flight-Control Systems.
FTRTFT 1992: 237-257 |
| 1991 |
|---|
| 5 | | Judith Crow,
John M. Rushby:
Model-Based Reconfiguration: Toward an Integration with Diagnosis.
AAAI 1991: 836-841 |
| 4 | | John M. Rushby:
Design Choices in Specification Languages and Verification Systems.
TPHOLs 1991: 195-204 |
| 1983 |
|---|
| 3 | | John M. Rushby,
Brian Randell:
A Distributed Secure System.
IEEE Symposium on Security and Privacy 1983: 127-135 |
| 1982 |
|---|
| 2 | | John M. Rushby:
Proof of separability: A verification technique for a class of a security kernels.
Symposium on Programming 1982: 352-367 |
| 1981 |
|---|
| 1 | | John M. Rushby:
Design and Verification of Secure Systems.
SOSP 1981: 12-21 |
