Travelled to:1 × India
1 × The Netherlands
3 × USA
Collaborated with:G.Gopalakrishnan S.S.Vakkalanka G.Li A.Vo M.Delisi D.Quinlan S.Sharma R.Thakur
Talks about:mpi (5) program (4) practic (2) formal (2) verif (2) standard (1) presenc (1) verifi (1) theori (1) symbol (1)
Person: Robert M. Kirby
DBLP: Kirby:Robert_M=
Contributed to:
2010
20092009
20082008Wrote 6 papers:
- PPoPP-2010-LiGKQ #source code #verification
- A symbolic verifier for CUDA programs (GL, GG, RMK, DQ), pp. 357–358.
- FM-2009-VakkalankaVGK #execution #semantics #theory and practice
- Reduced Execution Semantics of MPI: From Theory to Practice (SSV, AV, GG, RMK), pp. 724–740.
- PPoPP-2009-VoVDGKT #source code #verification
- Formal verification of practical MPI programs (AV, SSV, MD, GG, RMK, RT), pp. 261–270.
- CAV-2008-VakkalankaGK #order #reduction #source code #verification
- Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings (SSV, GG, RMK), pp. 66–79.
- PPoPP-2008-LiDGK #specification #standard
- Formal specification of the MPI-2.0 standard in TLA+ (GL, MD, GG, RMK), pp. 283–284.
- PPoPP-2008-VakkalankaSGK #model checking #named #source code
- ISP: a tool for model checking MPI programs (SSV, SS, GG, RMK), pp. 285–286.