Travelled to:1 × Canada
1 × Ireland
1 × Italy
1 × Japan
1 × Spain
1 × The Netherlands
2 × Finland
3 × Austria
3 × United Kingdom
6 × USA
Collaborated with:J.Hatcliff M.B.Dwyer J.Belt X.Deng P.Chalin S.A.DeLoach E.Rodríguez M.Hoosier J.C.Corbett W.Visser J.C.García-Ojeda J.Lee V.A.Kolesnikov V.P.Ranganath S.Laubach C.S.Pasareanu H.Zheng H.Thiagarajan O.Tkachuk D.Hardin T.Amtoft J.Hoag D.Greve T.Wallentine C.Flanagan G.T.Leavens W.Deng G.Jung R.Joehanes P.Courtieu M.Aponte T.Crolard Z.Zhang J.Guitton T.Jennings
Talks about:check (13) model (11) use (8) framework (5) softwar (5) program (5) symbol (5) specif (5) execut (5) contract (4)
Person: Robby
DBLP: Robby:
Facilitated 1 volumes:
SaEventsChContributed to:
2013
20132012
2012
2011
2009
2009
2008
20072006
2006
2006
2005
200520042004
20042003
200320012000Wrote 23 papers:
- HILT-2013-CourtieuACZRBHG #coq #formal method #runtime #semantics #towards #using
- Towards the formalization of SPARK 2014 semantics with explicit run-time checks using coq (PC, MVA, TC, ZZ, R, JB, JH, JG, TJ), pp. 21–22.
- ICSE-2013-HatcliffRCB #execution #framework #symbolic computation #verification
- Explicating symbolic execution (xSymExe): an evidence-based verification framework (JH, R, PC, JB), pp. 222–231.
- HILT-2012-BeltCHR #ada #automation #contract #using #verification
- Leading-edge Ada verification technologies: highly automated Ada contract checking using bakar kiasan (JB, PC, JH, R), pp. 3–4.
- SCAM-2012-ThiagarajanHBR #contract #data flow #developer
- Bakar Alir: Supporting Developers in Construction of Information Flow Contracts in SPARK (HT, JH, JB, R), pp. 132–137.
- SIGAda-2011-BeltHRCHD #contract #execution #symbolic computation #using
- Enhancing spark’s contract checking facilities using symbolic execution (JB, JH, R, PC, DH, XD), pp. 47–60.
- ESEC-FSE-2009-BeltRD #analysis #lightweight #optimisation #symbolic computation
- Sireum/Topi LDP: a lightweight semi-decision procedure for optimizing symbolic execution-based analyses (JB, R, XD), pp. 355–364.
- SAC-2009-Garcia-OjedaDR #design #editing #process
- agentTool process editor: supporting the design of tailored agent-based processes (JCGO, SAD, R), pp. 707–714.
- FM-2008-AmtoftHRRHG #contract #data flow #specification
- Specification and Checking of Software Contracts for Conditional Information Flow (TA, JH, ER, R, JH, DG), pp. 229–245.
- SEFM-2007-DengRH #algorithm #execution #object-oriented #source code #symbolic computation #towards
- Towards A Case-Optimal Symbolic Execution Algorithm for Analyzing Strong Properties of Object-Oriented Programs (XD, R, JH), pp. 273–282.
- ASE-2006-DengLR #bound #execution #named #symbolic computation
- Bogor/Kiasan: A k-bounded Symbolic Execution for Checking Strong Heap Properties of Open Systems (XD, JL, R), pp. 157–166.
- ASE-2006-RobbyDH #framework #model checking #using
- Domain-specific Model Checking Using The Bogor Framework (R, MBD, JH), pp. 369–370.
- FASE-2006-RobbyDK #design #flexibility #metric #predict #using
- Using Design Metrics for Predicting System Flexibility (R, SAD, VAK), pp. 184–198.
- TACAS-2006-DwyerHHRRW #concurrent #effectiveness #object-oriented #reduction #slicing #source code
- Evaluating the Effectiveness of Slicing for Model Reduction of Concurrent Object-Oriented Programs (MBD, JH, MH, VPR, R, TW), pp. 73–89.
- CAV-2005-DwyerHHR #framework #model checking #using
- Building Your Own Software Model Checker Using the Bogor Extensible Model Checking Framework (MBD, JH, MH, R), pp. 148–152.
- ECOOP-2005-RodriguezDFHLR #composition #concurrent #ml #multi #source code #specification #thread #verification
- Extending JML for Modular Specification and Verification of Multi-threaded Programs (ER, MBD, CF, JH, GTL, R), pp. 551–576.
- ASE-2004-DwyerRTV #interactive #model checking #order
- Analyzing Interaction Orderings with Model Checking (MBD, R, OT, WV), pp. 154–163.
- TACAS-2004-RobbyRDH #framework #model checking #specification #using
- Checking Strong Specifications Using an Extensible Software Model Checking Framework (R, ER, MBD, JH), pp. 404–420.
- VMCAI-2004-HatcliffRD #concurrent #model checking #object-oriented #specification #using #verification
- Verifying Atomicity Specifications for Concurrent Object-Oriented Software Using Model-Checking (JH, R, MBD), pp. 175–190.
- ESEC-FSE-2003-RobbyDH #framework #model checking #named
- Bogor: an extensible and highly-modular software model checking framework (R, MBD, JH), pp. 267–276.
- PEPM-2003-HatcliffDDJRR #component #corba #design #partial evaluation #slicing
- Slicing and partial evaluation of CORBA component model designs for avionics system (JH, WD, MBD, GJ, VPR, R), pp. 1–2.
- ICSE-2001-DwyerHJLPRZV #abstraction #finite #verification
- Tool-Supported Program Abstraction for Finite-State Verification (MBD, JH, RJ, SL, CSP, R, HZ, WV), pp. 177–187.
- ICSE-2000-CorbettDHLPRZ #finite #java #modelling #named #source code
- Bandera: extracting finite-state models from Java source code (JCC, MBD, JH, SL, CSP, R, HZ), pp. 439–448.
- ICSE-2000-CorbettDHR #interface #java #model checking #named #source code
- Bandera: a source-level interface for model checking Java programs (JCC, MBD, JH, R), pp. 762–765.