BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × China
1 × Denmark
1 × France
1 × Germany
1 × Greece
1 × India
1 × Ireland
1 × Spain
1 × Switzerland
1 × The Netherlands
1 × Vietnam
6 × USA
Collaborated with:
S.Owre N.Shankar G.Hamon L.M.d.Moura C.A.Muñoz P.Lincoln H.Rueß D.W.J.Stringer-Calvert F.W.v.Henke S.Rajan M.K.Srivas M.Sorea A.Tiwari
Talks about:
verif (8) formal (6) pvs (5) method (4) model (4) system (3) check (3) specif (2) mechan (2) deduct (2)

Person: John M. Rushby

DBLP DBLP: Rushby:John_M=

Contributed to:

SEFM 20092009
SEFM 20062006
CAV 20042004
FASE 20042004
IJCAR 20042004
SEFM 20042004
CAV 20002000
World Congress on Formal Methods 19991999
FM-Trends 19981998
ESEC/FSE 19971997
RE 19971997
TACAS 19971997
CAV 19961996
CAV 19931993
FME 19931993
CADE 19921992
SOSP 19811981

Wrote 20 papers:

SEFM-2009-Rushby #assurance #verification
Software Verification and System Assurance (JMR), pp. 3–10.
SEFM-2006-Rushby #verification
Harnessing Disruptive Innovation in Formal Verification (JMR), pp. 21–30.
SEFM-2006-Rushby06a #automation #formal method #named #tutorial
Tutorial: Automated Formal Methods with PVS, SAL, and Yices (JMR), p. 262.
CAV-2004-MouraORRSST
SAL 2 (LMdM, SO, HR, JMR, NS, MS, AT), pp. 496–500.
FASE-2004-HamonR #semantics
An Operational Semantics for Stateflow (GH, JMR), pp. 229–243.
IJCAR-2004-MouraORRS #deduction #embedded
The ICS Decision Procedures for Embedded Deduction (LMdM, SO, HR, JMR, NS), pp. 218–222.
SEFM-2004-HamonMR #generative #model checking #performance #testing
Generating Efficient Test Sets with a Model Checker (GH, LMdM, JMR), pp. 261–270.
CAV-2000-Rushby #diagrams #invariant #verification
Verification Diagrams Revisited: Disjunctive Invariants for Easy Verification (JMR), pp. 508–520.
FM-v1-1999-MunozR
Structural Embeddings: Mechanization with Method (CAM, JMR), pp. 452–471.
FM-v1-1999-Rushby #formal method #question
Mechanized Formal Methods: Where Next? (JMR), pp. 48–51.
FM-1998-OwreRSS #case study #experience #named
PVS: An Experience Report (SO, JMR, NS, DWJSC), pp. 338–345.
ESEC-FSE-1997-Rushby #specification #type system
Subtypes for Specifications (JMR), pp. 4–19.
RE-1997-Rushby #requirements
Calculating with Requirements (JMR), p. 144–?.
TACAS-1997-OwreRS #integration #model checking
Integration in PVS: Tables, Types, and Model Checking (SO, JMR, NS), pp. 366–383.
CAV-1996-OwreRRSS #model checking #named #proving #specification
PVS: Combining Specification, Proof Checking, and Model Checking (SO, SR, JMR, NS, MKS), pp. 411–414.
CAV-1996-Rushby #automation #deduction #formal method
Automated Deduction and Formal Methods (JMR), pp. 169–183.
CAV-1993-LincolnR #algorithm #consistency #fault #hybrid #interactive #verification
The Formal Verification of an Algorithm for Interactive Consistency under a Hybrid Fault Model (PL, JMR), pp. 292–304.
FME-1993-OwreRSH #architecture #fault tolerance #lessons learnt #verification
Formal Verification for Fault-Tolerant Architectures: Some Lessons Learned (SO, JMR, NS, FWvH), pp. 482–500.
CADE-1992-OwreRS #named #prototype #verification
PVS: A Prototype Verification System (SO, JMR, NS), pp. 748–752.
SOSP-1981-Rushby #design #verification
Design and Verification of Secure Systems (JMR), pp. 12–21.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.