Runtime Verification

• Inferring Event Stream Abstractions
  S. Kauffman, K. Havelund, R. Joshi, and S. Fischmeister
  Accepted for publication in Formal Methods in System Design (FMSD), 2018
  
• Modeling Rover Communication using Hierarchical State Machines with Scala
  K. Havelund, R. Joshi
  2nd International Workshop on the Timing Performance in Safety Engineering (TIPS 2017), Sep 2017
  
• Modeling and Monitoring of Hierarchical State Machines in Scala
  K. Havelund, R. Joshi
  9th International Workshop on Software Engineering for Resilient Systems (SERENE 2017), Sep 2017
  
• Towards a Logic for Inferring Properties of Event Streams
  S. Kauffman, K. Havelund, R. Joshi
  7th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA 2016), Oct 2016
  
• nfer - A Notation and System for Inferring Event Stream Abstractions
  S. Kauffman, K. Havelund, R. Joshi
  16th International Conference on Runtime Verification (RV 2016), Sep 2016
  
• Experience with Rule-Based Analysis of Spacecraft Logs
  K. Havelund, R. Joshi
  Third International Conference on Formal Techniques for Safety-Critical Systems (FTSCS), Nov 2014
  
• Comprehension of spacecraft telemetry using hierarchical specifications of behavior
  K. Havelund, R. Joshi
  International Conference on Formal Engineering Methods (ICFEM), Nov 2014
  

Model Checking and Testing

• Swarm Verification Techniques
  G. J. Holzmann, R. Joshi, A. Groce,
  IEEE Transactions on Software Engineering, Vol 37, No 6, Nov 2011
  
• Model driven code checking
  G. J. Holzmann, R. Joshi, A. Groce
  Automated Software Engineering Journal, Vol 15, Nr 3-4, pp 283-297, Dec 2008
  
• Swarm Verification
  G. J. Holzmann, R. Joshi, A. Groce
  Proceedings of the 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE), Sep 2008
  
• Verifying multi-threaded C programs with Spin
  A. Zaks and R. Joshi
  Proceedings of the 15th SPIN Workshop on Model Checking of Software, Aug 2008
  
• Tackling large verification problems with Swarms
  G. J. Holzmann, R. Joshi and A. Groce
  Proceedings of the 15th SPIN Workshop on Model Checking of Software, Aug 2008
  
• Putting flight software through the paces with testing, model checking, and constraint solving
  A. Groce, R. Joshi, R. Xu, G. J. Holzmann
  Proceedings of the 5th International Workshop on Constraints in Formal Verification (CFV), August 2008
  
• Random testing and model checking: building a common framework for nondeterministic exploration
  A. Groce and R. Joshi
  Proceedings of the 6th International Workshop on Dynamic Analysis (WODA), July 2008
  
• Automated testing of planning models
  K. Havelund, A. Groce, G. Holzmann, R. Joshi, M. Smith
  Proceedings of the 5th International Workshop on Model Checking and Artificial Intelligence (MOCHART), July 2008
  
• Exploiting traces in static program analysis
  A. Groce and R. Joshi
  International Journal on Software Tools for Technology Transfer (STTT), Vol 10, No 2, pp 131-144, Mar 2008
  (A somewhat expanded version of the TACAS paper below.)
• Extending model checking with dynamic analysis
  A. Groce and R. Joshi
  Proceedings of the Conference on Verification, Model Checking and Abstract Interpretation (VMCAI), Jan 2008, pp 142-156
  
• Randomized differential testing as a prelude to formal verification
  A. Groce, G. J. Holzmann, R. Joshi
  Proceedings of the 29th International Conference on Software Engineering (ICSE), May 2007
  
• Exploiting traces in static program analysis
  A. Groce and R. Joshi
  Proceedings of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Mar 2006
  
• Model-driven software verification
  G. J. Holzmann and R. Joshi
  Proceedings of the 11th International SPIN Workshop on Model Checking of Software, Apr 2004
  
• Checking cache coherence protocols with TLA+
  R. Joshi, L. Lamport, J. Matthews, S. Tasiran, M. Tuttle, Y. Yu
  Formal Methods in System Design, Vol 22, Nr 2, Mar 2003, pp 125-131
  

Theorem Proving and Constraint Solving

• Denali: A practical algorithm for generating optimal code
  R. Joshi, G. Nelson, Y. Zhou
  Transactions on Programming Languages and Systems (TOPLAS), Vol 22, Issue 6, Nov 2006, pp 967-989
  
• An Explicating Theorem Prover for Quantified Formulas
  Cormac Flanagan, Rajeev Joshi, James Saxe
  H.P. Laboratories Technical Report HPL-2004-199, 2004
  
• Automated Generation of Resource Configurations through Policies
  Akhil Sahai, Sharad Singhal, Vijay Machiraju, and Rajeev Joshi
  HP Laboratories Technical Report number HPL-2004-55, 2004
  
• Theorem proving with lazy proof explication
  Cormac Flanagan, Rajeev Joshi, Xinming Ou, James Saxe
  Proceedings of the 15th International Conference on Computer Aided Verification (CAV), Jul 2003
  
• Denali: A Goal-directed Superoptimizer
  Rajeev Joshi, Greg Nelson and Keith H. Randall
  Proceedings of the Conference on Programming Languages Design and Implementation (PLDI), Berlin, Germany, June 2002
  

Concurrency and Program Semantics

• Annotation Inference for Modular Checkers
  Cormac Flanagan, Rajeev Joshi and K. Rustan M. Leino
  Information Processing Letters, 77(2-4), Feb 2001, pp 97 108
  (Formalizes the theory behind the Houdini annotation inference tool.)
• Maximally Concurrent Programs
  Rajeev Joshi and Jayadev Misra
  Formal Aspects of Computing, Vol 12(2), 2000, pp 100 119
  
• A Semantic Approach to Secure Information Flow
  Rajeev Joshi and K. Rustan M. Leino
  Science of Computer Programming, Vol 37(1-3), 2000, pp 113 138
  Extends the ideas described in the MPC paper below
• A Semantic Approach to Secure Information Flow
  Rajeev Joshi and K. Rustan M. Leino
  Proceedings of the 4th International Conference on Mathematics of Program Construction (MPC), Marstrand, Sweden, June 1998
  
• Maximally Concurrent Programs [Shortened Version]
  Rajeev Joshi and Jayadev Misra
  Proceedings of the Conference on Principles of Distributed Computing (PODC), Portland, OR, July 2000
  
• Seuss: What the Doctor Ordered
  Lorenzo Alvisi, Rajeev Joshi, Calvin Lin and Jayadev Misra
  Proceedings of the Second International Workshop on Software Engineering for Parallel and Distributed Systems (PDSE), Boston, MA, May 1997
  

Invited Papers

• New Challenges in Model Checking
  G. J. Holzmann, R. Joshi, A. Groce
  Proceedings of the Symposium on 25 Years of Model Checking (25MC), Aug 2006
  
• A mini challenge: build a verifiable filesystem
  R. Joshi and G. J. Holzmann
  Proceedings of the 1st International Conference on Verified Software: Theories, Tools, Experiments (VSTTE), Oct 2005
  
• Reliable software systems design: defect prevention, detection, and containment
  G. J. Holzmann and R. Joshi
  Proceedings of the 1st International Conference on Verified Software: Theories, Tools, Experiments (VSTTE), Oct 2005
  
• A Projective Geometry Architecture for Scientific Computation
  Bharadwaj S. Amrutur, Rajeev Joshi, and Narendra K. Karmarkar
  Proceedings of the Conference on Application Specific Array Processors (ASAP), Berkeley, CA, Aug 1992
  

Selected Unpublished Notes

• On the Impossibility of Robust Solutions for Fair Resource Allocation
  Rajeev Joshi and Jayadev Misra
  University of Texas at Austin Technical Report number UTCS-99-14, April 1999
  
• Counterpoint: A UNITY proof with pure nondeterminism
  Rajeev Joshi
  March 1998 , Solves a problem (posed by J Moore) using the UNITY proof rules for pure nondeterminism
  
• Seuss for Java: Language Reference
  Rajeev Joshi
  February 1998, Defines the syntax of an adaptation of Jay Misra's Seuss notation to Java