John M. Rushby

78 papers A* 8A 7B 11C 5Misc 2Journal 12Unranked 32

Year	Rank	Type	Title / Venue / Authors
2014	J	`jnl`	Example of a Complementary Use of Model Checking and Human Performance Simulation. IEEE Trans. Hum. Mach. Syst. Gabriel Gelman, Karen M. Feigh, John M. Rushby
2014	—	`conf`	Safety envelope for security. HiCoNS Ashish Tiwari, Bruno Dutertre, Dejan Jovanovic, Thomas de Candia, Patrick Lincoln, John M. Rushby, Dorsa Sadigh, Sanjit A. Seshia
2013	B	`conf`	Example of a Complementary Use of Model Checking and Agent-Based Simulation. SMC Gabriel Gelman, Karen M. Feigh, John M. Rushby
2012	—	`conf`	The Versatile Synchronous Observer. SBMF John M. Rushby
2011	J	`jnl`	Formal Modeling and Analysis for Interactive Hybrid Systems. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. Ellen J. Bass, Karen M. Feigh, Elsa L. Gunter, John M. Rushby
2011	—	`conf`	Fractionated Software for Networked Cyber-Physical Systems: Research Directions and Long-Term Vision. Formal Modeling: Actors, Open Systems, Biological Systems Mark-Oliver Stehr, Carolyn L. Talcott, John M. Rushby, Patrick Lincoln, Minyoung Kim, Steven Cheung, Andy Poggio
2011	—	`conf`	From DSS to MILS - (Extended Abstract). Dependable and Historic Computing John M. Rushby
2011	Misc	`conf`	New challenges in certification for aircraft software. EMSOFT John M. Rushby
2011	B	`conf`	Toward a multi-method approach to formalizing human-automation interaction and human-human communications. SMC Ellen J. Bass, Matthew L. Bolton, Karen M. Feigh, Dennis Griffith, Elsa L. Gunter, William Mansky, John M. Rushby
2010	C	`conf`	Formalism in Safety Cases. SSS John M. Rushby
2009	B	`conf`	Software Verification and System Assurance. SEFM John M. Rushby
2008	B	`conf`	Runtime Certification. RV John M. Rushby
2007	J	`jnl`	An operational semantics for Stateflow. Int. J. Softw. Tools Technol. Transf. Grégoire Hamon, John M. Rushby
2007	J	`jnl`	Automated Formal Methods Enter the Mainstream. J. Univers. Comput. Sci. John M. Rushby
2007	A	`conf`	Distributed Secure Systems: Then and Now. ACSAC Brian Randell, John M. Rushby
2007	B	`conf`	Just-in-Time Certification. ICECCS John M. Rushby
2007	B	`conf`	What Use is Verified Software? ICECCS John M. Rushby
2006	B	`conf`	Harnessing Disruptive Innovation in Formal Verification. SEFM John M. Rushby
2006	—	`conf`	Hybrid Systems - And Everything Else. HSCC John M. Rushby
2006	—	`ch.`	PVS. The Seventeen Provers of the World Bart Jacobs, John M. Rushby
2006	B	`conf`	Tutorial: Automated Formal Methods with PVS, SAL, and Yices. SEFM John M. Rushby
2005	C	`conf`	An Evidential Tool Bus. ICFEM John M. Rushby
2005	—	`conf`	Automated Test Generation and Verified Software. VSTTE John M. Rushby
2004	B	`conf`	An Operational Semantics for Stateflow. FASE Grégoire Hamon, John M. Rushby
2004	B	`conf`	Generating Efficient Test Sets with a Model Checker. SEFM Grégoire Hamon, Leonardo Mendonça de Moura, John M. Rushby
2004	A	`conf`	Model Checking a Fault-Tolerant Startup Algorithm: From Design Exploration To Exhaustive Fault Simulation. DSN Wilfried Steiner, John M. Rushby, Maria Sorea, Holger Pfeifer
2004	A*	`conf`	SAL 2. CAV Leonardo Mendonça de Moura, Sam Owre, Harald Rueß, John M. Rushby, Natarajan Shankar, Maria Sorea, Ashish Tiwari
2004	A	`conf`	The ICS Decision Procedures for Embedded Deduction. IJCAR Leonardo Mendonça de Moura, Sam Owre, Harald Rueß, John M. Rushby, Natarajan Shankar
2003	J	`jnl`	Invisible formal methods for embedded control systems. Proc. IEEE Ashish Tiwari, Natarajan Shankar, John M. Rushby
2002	—	`conf`	An Overview of Formal Verification for the Time-Triggered Architecture. FTRTFT John M. Rushby
2002	A	`conf`	Formally Verified Byzantine Agreement in Presence of Link Faults. ICDCS Ulrich Schmid, Bettina Weiss, John M. Rushby
2001	Misc	`conf`	Bus Architectures for Safety-Critical Embedded Systems. EMSOFT John M. Rushby
2001	B	`conf`	Modeling the Human in Human Factors. SAFECOMP John M. Rushby
2000	—	`conf`	Analyzing Cockpit Interfaces Using Formal Methods. FM-Everywhere@FORTE/PSTV John M. Rushby
2000	C	`conf`	From Refutation to Verification. FORTE John M. Rushby
2000	—	`conf`	Theorem Proving for Verification. MOVEP John M. Rushby
2000	A*	`conf`	Verification Diagrams Revisited: Disjunctive Invariants for Easy Verification. CAV John M. Rushby
1999	—	`conf`	A case-study in component-based mechanical verification of fault-tolerant programs. WSS Sandeep S. Kulkarni, John M. Rushby, Natarajan Shankar
1999	—	`conf`	Integrated Formal Verification: Using Model Checking with Automated Abstraction, Invariant Generation, and Theorem Proving. SPIN John M. Rushby
1999	—	`conf`	Mechanized Formal Methods: Where Next? World Congress on Formal Methods John M. Rushby
1999	—	`conf`	Structural Embeddings: Mechanization with Method. World Congress on Formal Methods César A. Muñoz, John M. Rushby
1999	J	`jnl`	Systematic Formal Verification for Fault-Tolerant Time-Triggered Algorithms. IEEE Trans. Software Eng. John M. Rushby
1998	—	`conf`	PVS: An Experience Report. FM-Trends Sam Owre, John M. Rushby, Natarajan Shankar, David W. J. Stringer-Calvert
1998	J	`jnl`	Subtypes for Specifications: Predicate Subtyping in PVS. IEEE Trans. Software Eng. John M. Rushby, Sam Owre, Natarajan Shankar
1998	C	`conf`	Ubiquitous Abstraction: A New Approach to Mechanized Formal Verification. ICFEM John M. Rushby
1997	A	`conf`	Calculating with Requirements. RE John M. Rushby
1997	A	`conf`	Integration in PVS: Tables, Types, and Model Checking. TACAS Sam Owre, John M. Rushby, Natarajan Shankar
1997	—	`conf`	Low-Overhead Time-Triggered Group Membership. WDAG Shmuel Katz, Patrick Lincoln, John M. Rushby
1997	—	`conf`	Subtypes for Specifications. ESEC / SIGSOFT FSE John M. Rushby
1997	C	`conf`	Systematic Formal Verification of Interpreters. ICFEM David Cyrluk, John M. Rushby, Mandayam K. Srivas
1996	J	`jnl`	An Invitation to Formal Methods. Computer 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
1996	A*	`conf`	Automated Deduction and Formal Methods. CAV John M. Rushby
1996	J	`jnl`	Enhancing the Utility of Formal Methods. ACM Comput. Surv. John M. Rushby
1996	—	`conf`	Mechanized Formal Methods: Progress and Prospects. FSTTCS John M. Rushby
1996	A*	`conf`	PVS: Combining Specification, Proof Checking, and Model Checking. CAV Sam Owre, S. Rajan, John M. Rushby, Natarajan Shankar, Mandayam K. Srivas
1996	—	`conf`	Reconfiguration and Transient Recovery in State Machine Architectures. FTCS John M. Rushby
1995	J	`jnl`	Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS. IEEE Trans. Software Eng. Sam Owre, John M. Rushby, Natarajan Shankar, Friedrich W. von Henke
1995	—	`conf`	Mechanizing Formal Methods: Opportunities and Challenges. ZUM John M. Rushby
1995	—	`conf`	The Future of Formal Methods in Industry. ZUM Anthony Hall, David Lorge Parnas, Nico Plat, John M. Rushby, Chris T. Sennett
1994	A*	`conf`	A Formally Verifiable Algorithm for Clock Synchronization under a Hybrid Fault Model. PODC John M. Rushby
1994	—	`conf`	A Tutorial on Using PVS for Hardware Verification. TPCD Sam Owre, John M. Rushby, Natarajan Shankar, Mandayam K. Srivas
1994	—	`conf`	The PVS Verification System and PC/DC. FTRTFT John M. Rushby, Jens Ulrik Skakkebæk
1993	—	`conf`	A Formally Verified Algorithm for Interactive Consistency Under a Hybrid Fault Model. FTCS Patrick Lincoln, John M. Rushby
1993	—	`conf`	Formal Verification for Fault-Tolerant Architectures: Some Lessons Learned. FME Sam Owre, John M. Rushby, Natarajan Shankar, Friedrich W. von Henke
1993	J	`jnl`	Formal Verification of Algorithms for Critical Systems. IEEE Trans. Software Eng. John M. Rushby, Friedrich W. von Henke
1993	—	`conf`	Limits in Dependability (Panel). FTCS Jean-Claude Laprie, Gérard Le Lann, Michele Morganti, John M. Rushby
1993	A*	`conf`	The Formal Verification of an Algorithm for Interactive Consistency under a Hybrid Fault Model. CAV Patrick Lincoln, John M. Rushby
1993	—	`conf`	Using PVS to Prove Some Theorems Of David Parnas. HUG John M. Rushby, Mandayam K. Srivas
1992	—	`conf`	Formal Specification and Verification of a Fault-Masking and Transient-Recovery Model for Digital Flight-Control Systems. FTRTFT John M. Rushby
1992	A	`conf`	PVS: A Prototype Verification System. CADE Sam Owre, John M. Rushby, Natarajan Shankar
1991	—	`conf`	Design Choices in Specification Languages and Verification Systems. TPHOLs John M. Rushby
1991	—	`conf`	Formal verification of algorithms for critical systems. SIGSOFT John M. Rushby, Friedrich W. von Henke
1991	—	`conf`	From formal verification to silicon compilation. Compcon Jeffrey Joyce, Erwin Liu, John M. Rushby, Natarajan Shankar, Roberto Suaya, Friedrich W. von Henke
1991	A*	`conf`	Model-Based Reconfiguration: Toward an Integration with Diagnosis. AAAI Judith Crow, John M. Rushby
1983	—	`conf`	A Distributed Secure System. S&P John M. Rushby, Brian Randell
1983	J	`jnl`	A Distributed Secure System. Computer John M. Rushby, Brian Randell
1982	—	`conf`	Proof of separability: A verification technique for a class of a security kernels. Symposium on Programming John M. Rushby
1981	A*	`conf`	Design and Verification of Secure Systems. SOSP John M. Rushby