| 2021 | SOSP | Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3. | James Bornholt, Rajeev Joshi, Vytautas Astrauskas, Brendan Cully, Bernhard Kragl, Seth Markle, Kyle Sauri, Drew Schleit, Grant Slatton, Serdar Tasiran, Jacob Van Geffen, Andrew Warfield |
| 2018 | ISoLA | Modeling with Scala. | Klaus Havelund, Rajeev Joshi |
| 2017 | SAFECOMP | Modeling Rover Communication Using Hierarchical State Machines with Scala. | Klaus Havelund, Rajeev Joshi |
| 2016 | ISoLA | Towards a Logic for Inferring Properties of Event Streams. | Sean Kauffman, Rajeev Joshi, Klaus Havelund |
| 2016 | RV | nfer - A Notation and System for Inferring Event Stream Abstractions. | Sean Kauffman, Klaus Havelund, Rajeev Joshi |
| 2014 | ICFEM | Comprehension of Spacecraft Telemetry Using Hierarchical Specifications of Behavior. | Klaus Havelund, Rajeev Joshi |
| 2010 | IFM | Programming with Miracles. | Rajeev Joshi |
| 2008 | ISSTA | Random testing and model checking: building a common framework for nondeterministic exploration. | Alex Groce, Rajeev Joshi |
| 2008 | VMCAI | Extending Model Checking with Dynamic Analysis. | Alex Groce, Rajeev Joshi |
| 2007 | ICSE | Randomized Differential Testing as a Prelude to Formal Verification. | Alex Groce, Gerard J. Holzmann, Rajeev Joshi |
| 2006 | TACAS | Exploiting Traces in Program Analysis. | Alex Groce, Rajeev Joshi |
| 2004 | NOMS | Automated policy-based resource construction in utility computing environments. | Akhil Sahai, Sharad Singhal, Vijay Machiraju, Rajeev Joshi |
| 2003 | CAV | Theorem Proving Using Lazy Proof Explication. | Cormac Flanagan, Rajeev Joshi, Xinming Ou, James B. Saxe |
| 2002 | PLDI | Denali: A Goal-directed Superoptimizer. | Rajeev Joshi, Greg Nelson, Keith H. Randall |
| 2000 | PODC | Toward a theory of maximally concurrent programs (shortened version). | Rajeev Joshi, Jayadev Misra |
| 1998 | MPC | A Semantic Approach to Secure Information Flow. | K. Rustan M. Leino, Rajeev Joshi |