| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Ellen J. Bass, Karen M. Feigh, Elsa L. Gunter, John M. Rushby |
Formal Modeling and Analysis for Interactive Hybrid Systems.  |
ECEASST  |
2011 |
DBLP BibTeX RDF |
|
| 1 | Ellen J. Bass, Matthew L. Bolton, Karen M. Feigh, Dennis Griffith, Elsa L. Gunter, William Mansky, John M. Rushby |
Toward a multi-method approach to formalizing human-automation interaction and human-human communications. |
SMC |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | John M. Rushby |
New challenges in certification for aircraft software. |
EMSOFT |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Mark-Oliver Stehr, Carolyn L. Talcott, John M. Rushby, Patrick Lincoln, Minyoung Kim, Steven Cheung, Andy Poggio |
Fractionated Software for Networked Cyber-Physical Systems: Research Directions and Long-Term Vision. |
Formal Modeling: Actors, Open Systems, Biological Systems |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | John M. Rushby |
From DSS to MILS - (Extended Abstract). |
Dependable and Historic Computing |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | John M. Rushby |
Software Verification and System Assurance. |
SEFM |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | John M. Rushby |
Runtime Certification. |
RV |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | John M. Rushby |
Automated Formal Methods Enter the Mainstream. |
J. UCS |
2007 |
DBLP BibTeX RDF |
|
| 1 | Grégoire Hamon, John M. Rushby |
An operational semantics for Stateflow. |
STTT |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Brian Randell, John M. Rushby |
Distributed Secure Systems: Then and Now. |
ACSAC |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | John M. Rushby |
What Use is Verified Software? |
ICECCS |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | John M. Rushby |
Just-in-Time Certification. |
ICECCS |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | John M. Rushby |
Tutorial: Automated Formal Methods with PVS, SAL, and Yices. |
SEFM |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | John M. Rushby |
Harnessing Disruptive Innovation in Formal Verification. |
SEFM |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Bart Jacobs, John M. Rushby |
PVS. |
The Seventeen Provers of the World |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | John M. Rushby |
Hybrid Systems - And Everything Else. |
HSCC |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | John M. Rushby |
An Evidential Tool Bus. |
ICFEM |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | John M. Rushby |
Automated Test Generation and Verified Software. |
VSTTE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Grégoire Hamon, Leonardo Mendonça de Moura, John M. Rushby |
Generating Efficient Test Sets with a Model Checker. |
SEFM |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Leonardo Mendonça de Moura, Sam Owre, Harald Rueß, John M. Rushby, Natarajan Shankar |
The ICS Decision Procedures for Embedded Deduction. |
IJCAR |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
DBLP DOI BibTeX RDF |
|
| 1 | Grégoire Hamon, John M. Rushby |
An Operational Semantics for Stateflow. |
FASE |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Leonardo Mendonça de Moura, Sam Owre, Harald Rueß, John M. Rushby, Natarajan Shankar, Maria Sorea, Ashish Tiwari |
SAL 2. |
CAV |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Ashish Tiwari, Natarajan Shankar, John M. Rushby |
Invisible formal methods for embedded control systems. |
Proceedings of the IEEE |
2003 |
DBLP BibTeX RDF |
|
| 1 | Ulrich Schmid, Bettina Weiss, John M. Rushby |
Formally Verified Byzantine Agreement in Presence of Link Faults. (PDF / PS) |
ICDCS |
2002 |
DBLP DOI BibTeX RDF |
assumption coverage, formal verification, lower bounds, fault models, consensus, Byzantine agreement, Fault-tolerant distributed systems, link faults, impossibility results |
| 1 | John M. Rushby |
An Overview of Formal Verification for the Time-Triggered Architecture. |
FTRTFT |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | John M. Rushby |
Analyzing Cockpit Interfaces Using Formal Methods. |
Electr. Notes Theor. Comput. Sci. |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | John M. Rushby |
Bus Architectures for Safety-Critical Embedded Systems. |
EMSOFT |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | John M. Rushby |
Modeling the Human in Human Factors. |
SAFECOMP |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | John M. Rushby |
From Refutation to Verification. |
FORTE |
2000 |
DBLP BibTeX RDF |
|
| 1 | John M. Rushby |
Theorem Proving for Verification. |
MOVEP |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | John M. Rushby |
Verification Diagrams Revisited: Disjunctive Invariants for Easy Verification. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | John M. Rushby |
Systematic Formal Verification for Fault-Tolerant Time-Triggered Algorithms. |
IEEE Trans. Software Eng. |
1999 |
DBLP DOI BibTeX RDF |
time-triggered algorithms, Formal methods, formal verification, PVS, synchronous systems |
| 1 | John M. Rushby |
Integrated Formal Verification: Using Model Checking with Automated Abstraction, Invariant Generation, and Theorem Proving. |
SPIN |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | César Muñoz, John M. Rushby |
Structural Embeddings: Mechanization with Method. |
World Congress on Formal Methods |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | John M. Rushby |
Mechanized Formal Methods: Where Next? |
World Congress on Formal Methods |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Sandeep S. Kulkarni, John M. Rushby, Natarajan Shankar |
A case-study in component-based mechanical verification of fault-tolerant programs. |
WSS |
1999 |
DBLP BibTeX RDF |
|
| 1 | John M. Rushby, Sam Owre, Natarajan Shankar |
Subtypes for Specifications: Predicate Subtyping in PVS. |
IEEE Trans. Software Eng. |
1998 |
DBLP DOI BibTeX RDF |
typechecking, Formal methods, consistency, type systems, specification languages, subtypes, PVS |
| 1 | John M. Rushby |
Ubiquitous Abstraction: A New Approach to Mechanized Formal Verification. (PDF / PS) |
ICFEM |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Sam Owre, John M. Rushby, Natarajan Shankar, David W. J. Stringer-Calvert |
PVS: An Experience Report. |
FM-Trends |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | David Cyrluk, John M. Rushby, Mandayam K. Srivas |
Systematic Formal Verification of Interpreters. |
ICFEM |
1997 |
DBLP BibTeX RDF |
|
| 1 | Sam Owre, John M. Rushby, Natarajan Shankar |
Integration in PVS: Tables, Types, and Model Checking. |
TACAS |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | John M. Rushby |
Calculating with Requirements. |
RE |
1997 |
DBLP BibTeX RDF |
|
| 1 | Shmuel Katz, Patrick Lincoln, John M. Rushby |
Low-Overhead Time-Triggered Group Membership. |
WDAG |
1997 |
DBLP DOI BibTeX RDF |
time-triggered protocol, fault tolerance, formal modeling, group membership, synchronous algorithms |
| 1 | John M. Rushby |
Subtypes for Specifications. |
ESEC / SIGSOFT FSE |
1997 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
1996 |
DBLP DOI BibTeX RDF |
|
| 1 | John M. Rushby |
Enhancing the Utility of Formal Methods. |
ACM Comput. Surv. |
1996 |
DBLP DOI BibTeX RDF |
|
| 1 | John M. Rushby |
Reconfiguration and Transient Recovery in State Machine Architectures. |
FTCS |
1996 |
DBLP DOI BibTeX RDF |
|
| 1 | John M. Rushby |
Automated Deduction and Formal Methods. |
CAV |
1996 |
DBLP DOI BibTeX RDF |
|
| 1 | Sam Owre, S. Rajan, John M. Rushby, Natarajan Shankar, Mandayam K. Srivas |
PVS: Combining Specification, Proof Checking, and Model Checking. |
CAV |
1996 |
DBLP DOI BibTeX RDF |
|
| 1 | John M. Rushby |
Mechanized Formal Methods: Progress and Prospects. |
FSTTCS |
1996 |
DBLP DOI BibTeX RDF |
|
| 1 | 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. |
1995 |
DBLP DOI BibTeX RDF |
verification systems, fault tolerance, formal specification, formal methods, theorem proving, clock synchronization, PVS, Byzantine agreement, hardware verification, flight control |
| 1 | John M. Rushby |
Mechanizing Formal Methods: Opportunities and Challenges. |
ZUM |
1995 |
DBLP DOI BibTeX RDF |
|
| 1 | Anthony Hall, David Lorge Parnas, Nico Plat, John M. Rushby, Chris T. Sennett |
The Future of Formal Methods in Industry. |
ZUM |
1995 |
DBLP BibTeX RDF |
|
| 1 | Sam Owre, John M. Rushby, Natarajan Shankar, Mandayam K. Srivas |
A Tutorial on Using PVS for Hardware Verification. |
TPCD |
1994 |
DBLP DOI BibTeX RDF |
|
| 1 | John M. Rushby |
A Formally Verifiable Algorithm for Clock Synchronization under a Hybrid Fault Model. |
PODC |
1994 |
DBLP DOI BibTeX RDF |
|
| 1 | John M. Rushby, Jens Ulrik Skakkebæk |
The PVS Verification System and PC/DC. |
FTRTFT |
1994 |
DBLP BibTeX RDF |
|
| 1 | John M. Rushby, Friedrich W. von Henke |
Formal Verification of Algorithms for Critical Systems. |
IEEE Trans. Software Eng. |
1993 |
DBLP DOI BibTeX RDF |
machine-checked verification, Byzantine fault-tolerant algorithm, digital flight control system, fault-tolerant synchronization, EHDM system, formal specification, formal specification, formal verification, fault tolerant computing, software reliability, safety, synchronisation, critical systems |
| 1 | Sam Owre, John M. Rushby, Natarajan Shankar, Friedrich W. von Henke |
Formal Verification for Fault-Tolerant Architectures: Some Lessons Learned. |
FME |
1993 |
DBLP DOI BibTeX RDF |
|
| 1 | John M. Rushby, Mandayam K. Srivas |
Using PVS to Prove Some Theorems Of David Parnas. |
HUG |
1993 |
DBLP DOI BibTeX RDF |
|
| 1 | Patrick Lincoln, John M. Rushby |
A Formally Verified Algorithm for Interactive Consistency Under a Hybrid Fault Model. |
FTCS |
1993 |
DBLP DOI BibTeX RDF |
|
| 1 | Jean-Claude Laprie, Gérard Le Lann, Michele Morganti, John M. Rushby |
Limits in Dependability (Panel). |
FTCS |
1993 |
DBLP DOI BibTeX RDF |
|
| 1 | Patrick Lincoln, John M. Rushby |
The Formal Verification of an Algorithm for Interactive Consistency under a Hybrid Fault Model. |
CAV |
1993 |
DBLP DOI BibTeX RDF |
|
| 1 | Sam Owre, John M. Rushby, Natarajan Shankar |
PVS: A Prototype Verification System. |
CADE |
1992 |
DBLP DOI BibTeX RDF |
|
| 1 | John M. Rushby |
Formal Specification and Verification of a Fault-Masking and Transient-Recovery Model for Digital Flight-Control Systems. |
FTRTFT |
1992 |
DBLP DOI BibTeX RDF |
|
| 1 | John M. Rushby |
Design Choices in Specification Languages and Verification Systems. |
TPHOLs |
1991 |
DBLP BibTeX RDF |
|
| 1 | Judith Crow, John M. Rushby |
Model-Based Reconfiguration: Toward an Integration with Diagnosis. |
AAAI |
1991 |
DBLP BibTeX RDF |
|
| 1 | John M. Rushby, Brian Randell |
A Distributed Secure System. |
IEEE Symposium on Security and Privacy |
1983 |
DBLP BibTeX RDF |
|
| 1 | John M. Rushby |
Proof of separability: A verification technique for a class of a security kernels. |
Symposium on Programming |
1982 |
DBLP DOI BibTeX RDF |
|
| 1 | John M. Rushby |
Design and Verification of Secure Systems. |
SOSP |
1981 |
DBLP DOI BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")