Search the dblp DataBase

Publications of Author

1. John Matthews, John Launchbury
   Elementary Microarchitecture Algebra. [Citation Graph (0, 0)][DBLP]
   CAV, 1999, pp:288-300 [Conf]
   
2. Byron Cook, John Launchbury, John Matthews, Richard B. Kieburtz
   Formal Verification of Explicitly Parallel Microprocessors. [Citation Graph (0, 0)][DBLP]
   CHARME, 1999, pp:23-36 [Conf]
   
3. John Matthews, Byron Cook, John Launchbury
   Microprocessor Specification in Hawk. [Citation Graph (0, 0)][DBLP]
   ICCL, 1998, pp:90-101 [Conf]
   
4. John Matthews, Charles U. Martel
   Parallel Algorithms Using Unreliable Broadcasts. [Citation Graph (0, 0)][DBLP]
   IPPS, 1996, pp:692-696 [Conf]
   
5. John Matthews, J. Strother Moore, Sandip Ray, Daron Vroon
   Verification Condition Generation Via Theorem Proving. [Citation Graph (0, 0)][DBLP]
   LPAR, 2006, pp:362-376 [Conf]
   
6. Gary S. Tyson, Matthew K. Farrens, John Matthews, Andrew R. Pleszkun
   A modified approach to data cache management. [Citation Graph (0, 0)][DBLP]
   MICRO, 1995, pp:93-103 [Conf]
   
7. Sava Krstic, John Matthews
   Semantics of the reFL^ect language. [Citation Graph (0, 0)][DBLP]
   PPDP, 2004, pp:32-42 [Conf]
   
8. Srinivasan Tridandapani, Anton T. Dahbura, Arun K. Somani, Charles U. Martel, John Matthews
   Free Performance and Fault Tolerance: Using System Idle Capacity Efficiently (Panel). [Citation Graph (0, 0)][DBLP]
   SIGMETRICS, 1995, pp:60-61 [Conf]
   
9. Brian Huffman, John Matthews, Peter White
   Axiomatic Constructor Classes in Isabelle/HOLCF. [Citation Graph (0, 0)][DBLP]
   TPHOLs, 2005, pp:147-162 [Conf]
   
10. Sava Krstic, John Matthews
    Inductive Invariants for Nested Recursion. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2003, pp:253-269 [Conf]
    
11. John Matthews
    Recursive Function Definition over Coinductive Types. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 1999, pp:73-90 [Conf]
    
12. Sava Krstic, John Matthews
    Verifying BDD Algorithms through Monadic Interpretation. [Citation Graph (0, 0)][DBLP]
    VMCAI, 2002, pp:182-195 [Conf]
    
13. Lee Pike, Mark Shields, John Matthews
    A verifying core for a cryptographic language compiler. [Citation Graph (0, 0)][DBLP]
    ACL2, 2006, pp:1-10 [Conf]
    
14. Rajeev Joshi, Leslie Lamport, John Matthews, Serdar Tasiran, Mark R. Tuttle, Yuan Yu
    Checking Cache-Coherence Protocols with TLA⁺. [Citation Graph (0, 0)][DBLP]
    Formal Methods in System Design, 2003, v:22, n:2, pp:125-131 [Journal]
    
15. 
    Specifying and verifying systems with TLA+. [Citation Graph (, )][DBLP]
    
    
16. 
    Imperative Functional Programming with Isabelle/HOL. [Citation Graph (, )][DBLP]
    
    
17. 
    Pragmatic equivalence and safety checking in Cryptol. [Citation Graph (, )][DBLP]
    
    
18. 
    A network rate management protocol with TCP congestion control and fairness for all. [Citation Graph (, )][DBLP]