Google
Google Scholar
MS Academic
CiteSeerX
CORE
Semantic ScholarJohn M. Rushby
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2010 – 2019
- 2014
[j13]Gabriel Gelman, Karen M. Feigh, John M. Rushby:
Example of a Complementary Use of Model Checking and Human Performance Simulation. IEEE Trans. Hum. Mach. Syst. 44(5): 576-590 (2014)- [c63]Ashish Tiwari, Bruno Dutertre, Dejan Jovanovic, Thomas de Candia, Patrick Lincoln, John M. Rushby, Dorsa Sadigh, Sanjit A. Seshia:
Safety envelope for security. HiCoNS 2014: 85-94 - 2013
- [c62]Gabriel Gelman, Karen M. Feigh, John M. Rushby:
Example of a Complementary Use of Model Checking and Agent-Based Simulation. SMC 2013: 900-905 - 2012
- [c61]John M. Rushby:
The Versatile Synchronous Observer. SBMF 2012: 1 - 2011
- [j12]Ellen J. Bass, Karen M. Feigh, Elsa L. Gunter, John M. Rushby:
Formal Modeling and Analysis for Interactive Hybrid Systems. ECEASST 45 (2011) - [c60]John M. Rushby:
From DSS to MILS - (Extended Abstract). Dependable and Historic Computing 2011: 53-57 - [c59]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: 110-143 - [c58]John M. Rushby:
New challenges in certification for aircraft software. EMSOFT 2011: 211-218 - [c57]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: 1817-1824 - 2010
- [c56]John M. Rushby:
Formalism in Safety Cases. SSS 2010: 3-17
2000 – 2009
- 2009
- [c55]John M. Rushby:
Software Verification and System Assurance. SEFM 2009: 3-10 - 2008
- [c54]John M. Rushby:
Runtime Certification. RV 2008: 21-35 - 2007
- [j11]John M. Rushby:
Automated Formal Methods Enter the Mainstream. J. UCS 13(5): 650-660 (2007) - [j10]Grégoire Hamon, John M. Rushby:
An operational semantics for Stateflow. Int. J. Softw. Tools Technol. Transf. 9(5-6): 447-456 (2007) - [c53]Brian Randell, John M. Rushby:
Distributed Secure Systems: Then and Now. ACSAC 2007: 177-199 - [c52]John M. Rushby:
Just-in-Time Certification. ICECCS 2007: 15-24 - [c51]John M. Rushby:
What Use is Verified Software? ICECCS 2007: 270-276 - 2006
- [c50]John M. Rushby:
Hybrid Systems - And Everything Else. HSCC 2006: 3 - [c49]John M. Rushby:
Harnessing Disruptive Innovation in Formal Verification. SEFM 2006: 21-30 - [c48]John M. Rushby:
Tutorial: Automated Formal Methods with PVS, SAL, and Yices. SEFM 2006: 262 - [p1]Bart Jacobs, John M. Rushby:
PVS. The Seventeen Provers of the World 2006: 24-27 - 2005
- [c47]John M. Rushby:
An Evidential Tool Bus. ICFEM 2005: 36-36 - [c46]John M. Rushby:
Automated Test Generation and Verified Software. VSTTE 2005: 161-172 - 2004
- [c45]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 - [c44]Leonardo Mendonça de Moura, Sam Owre, Harald Rueß, John M. Rushby, Natarajan Shankar, Maria Sorea, Ashish Tiwari:
SAL 2. CAV 2004: 496-500 - [c43]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 - [c42]Grégoire Hamon, John M. Rushby:
An Operational Semantics for Stateflow. FASE 2004: 229-243 - [c41]Grégoire Hamon, Leonardo Mendonça de Moura, John M. Rushby:
Generating Efficient Test Sets with a Model Checker. SEFM 2004: 261-270 - 2003
- [j9]Ashish Tiwari, Natarajan Shankar, John M. Rushby:
Invisible formal methods for embedded control systems. Proceedings of the IEEE 91(1): 29-39 (2003) - 2002
- [c40]John M. Rushby:
An Overview of Formal Verification for the Time-Triggered Architecture. FTRTFT 2002: 83-106 - [c39]Ulrich Schmid, Bettina Weiss, John M. Rushby:
Formally Verified Byzantine Agreement in Presence of Link Faults. ICDCS 2002: 608-616 - 2001
- [j8]John M. Rushby:
Analyzing Cockpit Interfaces Using Formal Methods. Electron. Notes Theor. Comput. Sci. 43: 1-14 (2001) - [c38]John M. Rushby:
Bus Architectures for Safety-Critical Embedded Systems. EMSOFT 2001: 306-323 - [c37]John M. Rushby:
Modeling the Human in Human Factors. SAFECOMP 2001: 86-91 - 2000
- [c36]John M. Rushby:
Verification Diagrams Revisited: Disjunctive Invariants for Easy Verification. CAV 2000: 508-520 - [c35]John M. Rushby:
From Refutation to Verification. FORTE 2000: 369-374 - [c34]John M. Rushby:
Theorem Proving for Verification. MOVEP 2000: 39-57
1990 – 1999
- 1999
- [j7]John M. Rushby:
Systematic Formal Verification for Fault-Tolerant Time-Triggered Algorithms. IEEE Trans. Software Eng. 25(5): 651-660 (1999) - [c33]John M. Rushby:
Mechanized Formal Methods: Where Next? World Congress on Formal Methods 1999: 48-51 - [c32]César A. Muñoz, John M. Rushby:
Structural Embeddings: Mechanization with Method. World Congress on Formal Methods 1999: 452-471 - [c31]John M. Rushby:
Integrated Formal Verification: Using Model Checking with Automated Abstraction, Invariant Generation, and Theorem Proving. SPIN 1999: 1-11 - [c30]Sandeep S. Kulkarni, John M. Rushby, Natarajan Shankar:
A case-study in component-based mechanical verification of fault-tolerant programs. WSS 1999: 33-40 - 1998
- [j6]John M. Rushby, Sam Owre, Natarajan Shankar:
Subtypes for Specifications: Predicate Subtyping in PVS. IEEE Trans. Software Eng. 24(9): 709-720 (1998) - [c29]Sam Owre, John M. Rushby, Natarajan Shankar, David W. J. Stringer-Calvert:
PVS: An Experience Report. FM-Trends 1998: 338-345 - [c28]John M. Rushby:
Ubiquitous Abstraction: A New Approach to Mechanized Formal Verification. ICFEM 1998: 176-179 - 1997
- [c27]John M. Rushby:
Subtypes for Specifications. ESEC / SIGSOFT FSE 1997: 4-19 - [c26]David Cyrluk, John M. Rushby, Mandayam K. Srivas:
Systematic Formal Verification of Interpreters. ICFEM 1997: 140-150 - [c25]John M. Rushby:
Calculating with Requirements. RE 1997: 144- - [c24]Sam Owre, John M. Rushby, Natarajan Shankar:
Integration in PVS: Tables, Types, and Model Checking. TACAS 1997: 366-383 - [c23]Shmuel Katz, Patrick Lincoln, John M. Rushby:
Low-Overhead Time-Triggered Group Membership. WDAG 1997: 155-169 - 1996
- [j5]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) - [j4]John M. Rushby:
Enhancing the Utility of Formal Methods. ACM Comput. Surv. 28(4es): 123 (1996) - [c22]John M. Rushby:
Automated Deduction and Formal Methods. CAV 1996: 169-183 - [c21]Sam Owre, S. Rajan, John M. Rushby, Natarajan Shankar, Mandayam K. Srivas:
PVS: Combining Specification, Proof Checking, and Model Checking. CAV 1996: 411-414 - [c20]John M. Rushby:
Mechanized Formal Methods: Progress and Prospects. FSTTCS 1996: 43-51 - [c19]John M. Rushby:
Reconfiguration and Transient Recovery in State Machine Architectures. FTCS 1996: 6-15 - 1995
- [j3]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) - [c18]John M. Rushby:
Mechanizing Formal Methods: Opportunities and Challenges. ZUM 1995: 105-113 - [c17]Anthony Hall, David Lorge Parnas, Nico Plat, John M. Rushby, Chris T. Sennett:
The Future of Formal Methods in Industry. ZUM 1995: 237-242 - 1994
- [c16]John M. Rushby, Jens Ulrik Skakkebæk:
The PVS Verification System and PC/DC. FTRTFT 1994: 777 - [c15]John M. Rushby:
A Formally Verifiable Algorithm for Clock Synchronization under a Hybrid Fault Model. PODC 1994: 304-313 - [c14]Sam Owre, John M. Rushby, Natarajan Shankar, Mandayam K. Srivas:
A Tutorial on Using PVS for Hardware Verification. TPCD 1994: 258-279 - 1993
- [j2]John M. Rushby, Friedrich W. von Henke:
Formal Verification of Algorithms for Critical Systems. IEEE Trans. Software Eng. 19(1): 13-23 (1993) - [c13]Patrick Lincoln, John M. Rushby:
The Formal Verification of an Algorithm for Interactive Consistency under a Hybrid Fault Model. CAV 1993: 292-304 - [c12]Sam Owre, John M. Rushby, Natarajan Shankar, Friedrich W. von Henke:
Formal Verification for Fault-Tolerant Architectures: Some Lessons Learned. FME 1993: 482-500 - [c11]Patrick Lincoln, John M. Rushby:
A Formally Verified Algorithm for Interactive Consistency Under a Hybrid Fault Model. FTCS 1993: 402-411 - [c10]Jean-Claude Laprie, Gérard Le Lann, Michele Morganti, John M. Rushby:
Limits in Dependability (Panel). FTCS 1993: 608-613 - [c9]John M. Rushby, Mandayam K. Srivas:
Using PVS to Prove Some Theorems Of David Parnas. HUG 1993: 163-173 - 1992
- [c8]Sam Owre, John M. Rushby, Natarajan Shankar:
PVS: A Prototype Verification System. CADE 1992: 748-752 - [c7]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
- [c6]Judith Crow, John M. Rushby:
Model-Based Reconfiguration: Toward an Integration with Diagnosis. AAAI 1991: 836-841 - [c5]Jeffrey Joyce, Erwin Liu, John M. Rushby, Natarajan Shankar, Roberto Suaya, Friedrich W. von Henke:
From formal verification to silicon compilation. Compcon 1991: 450-455 - [c4]John M. Rushby:
Design Choices in Specification Languages and Verification Systems. TPHOLs 1991: 195-204
1980 – 1989
- 1983
- [j1]John M. Rushby, Brian Randell:
A Distributed Secure System. IEEE Computer 16(7): 55-67 (1983) - [c3]John M. Rushby, Brian Randell:
A Distributed Secure System. IEEE Symposium on Security and Privacy 1983: 127-135 - 1982
- [c2]John M. Rushby:
Proof of separability: A verification technique for a class of a security kernels. Symposium on Programming 1982: 352-367 - 1981
- [c1]John M. Rushby:
Design and Verification of Secure Systems. SOSP 1981: 12-21
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
load content from web.archive.org
Privacy notice: By enabling the option above, your browser will contact the API of web.archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org and opencitations.net to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy.
Citation data
Add a list of citing articles from to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy.
Tweets on dblp homepage
Show tweets from 
on the dblp homepage.
Privacy notice: By enabling the option above, your browser will contact twitter.com and twimg.com to load tweets curated by our Twitter accout. At the same time, Twitter will persitently store several cookies with your web browser. While we did signal Twitter to not track our users by setting the "dnt" flag, we do not have any control over how Twitter uses your data. So please proceed with care and consider checking the Twitter privacy policy.
last updated on 2020-05-20 00:14 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
the dblp computer science bibliography is funded by:
