These web pages use cascading style sheet features for
formatting. You may still browse the text of the site, but for best
results, use a modern CSS-enabled browser.
-
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
-
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
-
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
-
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
-
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