Bandera: extracting finite-state models from Java source code. - James C. Corbett; Matthew B. Dwyer; John Hatcliff; Shawn Laubach; Corina S. Pasareanu; Robby; Hongjun Zheng (ICSE, 2000)

Bandera: a source-level interface for model checking Java programs. - James C. Corbett; Matthew B. Dwyer; John Hatcliff; Robby (ICSE, 2000)

A Language Framework for Expressing Checkable Properties of Dynamic Software. - James C. Corbett; Matthew B. Dwyer; John Hatcliff; Robby (SPIN, 2000)

Tool-Supported Program Abstraction for Finite-State Verification. - Matthew B. Dwyer; John Hatcliff; Roby Joehanes; Shawn Laubach; Corina S. Pasareanu; Robby; Hongjun Zheng; Willem Visser (ICSE, 2001)

Foundations of the Bandera Abstraction Tools. - John Hatcliff; Matthew B. Dwyer; Corina S. Pasareanu; Robby (The Essence of Computation, 2002)

Model-Checking Middleware-Based Event-Driven Real-Time Embedded Software. - Xianghua Deng; Matthew B. Dwyer; John Hatcliff; Georg Jung; Robby; Gurdip Singh (FMCO, 2002)

Expressing checkable properties of dynamic systems: the Bandera Specification Language. - James C. Corbett; Matthew B. Dwyer; John Hatcliff; Robby (Int. J. Softw. Tools Technol. Transf., 2002)

Space Reductions for Model Checking Quasi-Cyclic Systems. - Matthew B. Dwyer; Robby; Xianghua Deng; John Hatcliff (EMSOFT, 2003)

Slicing and partial evaluation of CORBA component model designs for avionics system. - John Hatcliff; William Deng; Matthew B. Dwyer; Georg Jung; Venkatesh Prasad Ranganath; Robby (PEPM, 2003)

Bogor: an extensible and highly-modular software model checking framework. - Robby; Matthew B. Dwyer; John Hatcliff (ESEC / SIGSOFT FSE, 2003)

Space-Reduction Strategies for Model Checking Dynamic Software. - Robby; Matthew B. Dwyer; John Hatcliff; Radu Iosif (SoftMC@CAV, 2003)

A Flexible Framework for the Estimation of Coverage Metrics in Explicit State Software Model Checking. - Edwin Rodríguez; Matthew B. Dwyer; John Hatcliff; Robby (CASSIS, 2004)

A Case Study in Domain-customized Model Checking for Real-time Component Software. - Matthew Hoosier; John Hatcliff; Robby; Matthew B. Dwyer (ISoLA (Preliminary proceedings), 2004)

Analyzing Interaction Orderings with Model Checking. - Matthew B. Dwyer; Robby; Oksana Tkachuk; Willem Visser (ASE, 2004)

Checking Strong Specifications Using an Extensible Software Model Checking Framework. - Robby; Edwin Rodríguez; Matthew B. Dwyer; John Hatcliff (TACAS, 2004)

Verifying Atomicity Specifications for Concurrent Object-Oriented Software Using Model-Checking. - John Hatcliff; Robby; Matthew B. Dwyer (VMCAI, 2004)

Exploiting Object Escape and Locking Information in Partial-Order Reductions for Concurrent Object-Oriented Programs. - Matthew B. Dwyer; John Hatcliff; Robby; Venkatesh Prasad Ranganath (Formal Methods Syst. Des., 2004)

Building Your Own Software Model Checker Using the Bogor Extensible Model Checking Framework. - Matthew B. Dwyer; John Hatcliff; Matthew Hoosier; Robby (CAV, 2005)

Extending JML for Modular Specification and Verification of Multi-threaded Programs. - Edwin Rodríguez; Matthew B. Dwyer; Cormac Flanagan; John Hatcliff; Gary T. Leavens; Robby (ECOOP, 2005)

Using Design Metrics for Predicting System Flexibility. - Robby; Scott A. DeLoach; Valeriy A. Kolesnikov (FASE, 2006)

Kiasan: A Verification and Test-Case Generation Framework for Java Based on Symbolic Execution. - Xianghua Deng; Robby; John Hatcliff (ISoLA, 2006)

Bogor/Kiasan: A k-bounded Symbolic Execution for Checking Strong Heap Properties of Open Systems. - Xianghua Deng; Jooyong Lee; Robby (ASE, 2006)

Domain-specific Model Checking Using The Bogor Framework. - Robby; Matthew B. Dwyer; John Hatcliff (ASE, 2006)

Evaluating the Effectiveness of Slicing for Model Reduction of Concurrent Object-Oriented Programs. - Matthew B. Dwyer; John Hatcliff; Matthew Hoosier; Venkatesh Prasad Ranganath; Robby; Todd Wallentine (TACAS, 2006)

Bogor: A Flexible Framework for Creating Software Model Checkers. - Robby; Matthew B. Dwyer; John Hatcliff (TAIC PART, 2006)

Checking JML specifications using an extensible software model checking framework. - Robby; Edwin Rodríguez; Matthew B. Dwyer; John Hatcliff (Int. J. Softw. Tools Technol. Transf., 2006)

O-MaSE: A Customizable Approach to Developing Multiagent Development Processes. - Juan C. García-Ojeda; Scott A. DeLoach; Robby; Walamitien H. Oyenan; Jorge L. Valenzuela (AOSE, 2007)

Trace-Based Specification of Law and Guidance Policies for Multi-Agent Systems. - Scott J. Harmon; Scott A. DeLoach; Robby (ESAW, 2007)

Formal Software Analysis Emerging Trends in Software Model Checking. - Matthew B. Dwyer; John Hatcliff; Robby; Corina S. Pasareanu; Willem Visser (FOSE, 2007)

Towards A Case-Optimal Symbolic Execution Algorithm for Analyzing Strong Properties of Object-Oriented Programs. - Xianghua Deng; Robby; John Hatcliff (SEFM, 2007)

Specification and Checking of Software Contracts for Conditional Information Flow. - Torben Amtoft; John Hatcliff; Edwin Rodríguez; Robby; Jonathan Hoag; David A. Greve (FM, 2008)

Leveraging Organizational Guidance Policies with Learning to Self-Tune Multiagent Systems. - Scott J. Harmon; Scott A. DeLoach; Robby; Doina Caragea (SASO, 2008)

agentTool III: from process definition to code generation. - Juan C. García-Ojeda; Scott A. DeLoach; Robby (AAMAS (2), 2009)

From abstract qualities to concrete specification using guidance policies. - Scott J. Harmon; Scott A. DeLoach; Robby (AAMAS (2), 2009)

Preliminary design of a unified JML representation and software infrastructure. - Robby; Patrice Chalin (FTfJP@ECOOP, 2009)

Abstract Requirement Analysis in Multiagent System Design. - Scott J. Harmon; Scott A. DeLoach; Robby (IAT, 2009)

agentTool process editor: supporting the design of tailored agent-based processes. - Juan C. García-Ojeda; Scott A. DeLoach; Robby (SAC, 2009)

Sireum/Topi LDP: a lightweight semi-decision procedure for optimizing symbolic execution-based analyses. - Jason Belt; Robby; Xianghua Deng (ESEC/SIGSOFT FSE, 2009)

Specification and Checking of Software Contracts for Conditional Information Flow. - Torben Amtoft; John Hatcliff; Edwin Rodríguez; Robby; Jonathan Hoag; David A. Greve (Design and Verification of Microprocessor Systems for High-Assurance Applications, 2010)

Towards an industrial grade IVE for Java and next generation research platform for JML. - Patrice Chalin; Robby; Perry R. James; Jooyong Lee; George Karabotsos (Int. J. Softw. Tools Technol. Transf., 2010)

Bakar Kiasan: Flexible Contract Checking for Critical Systems Using Symbolic Execution. - Jason Belt; John Hatcliff; Robby; Patrice Chalin; David S. Hardin; Xianghua Deng (NASA Formal Methods, 2011)

Enhancing spark's contract checking facilities using symbolic execution. - Jason Belt; John Hatcliff; Robby; Patrice Chalin; David S. Hardin; Xianghua Deng (SIGAda, 2011)

Efficient Symbolic Execution of Value-Based Data Structures for Critical Systems. - Jason Belt; Robby; Patrice Chalin; John Hatcliff; Xianghua Deng (NASA Formal Methods, 2012)

Bakar Alir: Supporting Developers in Construction of Information Flow Contracts in SPARK. - Hariharan Thiagarajan; John Hatcliff; Jason Belt; Robby (SCAM, 2012)

Leading-edge Ada verification technologies: highly automated Ada contract checking using bakar kiasan. - Jason Belt; Patrice Chalin; John Hatcliff; Robby (HILT, 2012)

Efficient and formal generalized symbolic execution. - Xianghua Deng; Jooyong Lee; Robby (Autom. Softw. Eng., 2012)

Past expression: encapsulating pre-states at post-conditions by means of AOP. - Jooyong Yi; Robby; Xianghua Deng; Abhik Roychoudhury (AOSD, 2013)

Explicating symbolic execution (xSymExe): an evidence-based verification framework. - John Hatcliff; Robby; Patrice Chalin; Jason Belt (ICSE, 2013)

Towards the formalization of SPARK 2014 semantics with explicit run-time checks using coq. - Pierre Courtieu; Maria-Virginia Aponte; Tristan Crolard; Zhi Zhang; Robby; Jason Belt; John Hatcliff; Jérôme Guitton; Trevor Jennings (HILT, 2013)

Towards an AADL-Based Definition of App Architecture for Medical Application Platforms. - Sam Procter; John Hatcliff; Robby (FHIES/SEHC, 2014)

Communication patterns for interconnecting and composing medical systems. - Venkatesh-Prasad Ranganath; Yu Jin Kim; John Hatcliff; Robby (EMBC, 2015)

Ecosphere Principles for Medical Application Platforms. - Yu Jin Kim; Sam Procter; John Hatcliff; Venkatesh-Prasad Ranganath; Robby (ICHI, 2015)

Focused Certification of an Industrial Compilation and Static Verification Toolchain. - Zhi Zhang; Robby; John Hatcliff; Yannick Moy; Pierre Courtieu (SEFM, 2017)

A Unified Approach for Modeling, Developing, and Assuring Critical Systems. - John Hatcliff; Brian R. Larson; Jason Belt; Robby; Yi Zhang 051 (ISoLA (1), 2018)

Model-Based Development for High-Assurance Embedded Systems. - Robby; John Hatcliff; Jason Belt (ISoLA (1), 2018)

Amandroid: A Precise and General Inter-component Data Flow Analysis Framework for Security Vetting of Android Apps. - Fengguo Wei; Sankardas Roy; Xinming Ou; Robby (ACM Trans. Priv. Secur., 2018)

HAMR: An AADL Multi-platform Code Generation Toolset. - John Hatcliff; Jason Belt; Robby; Todd Carpenter (ISoLA, 2021)

Slang: The Sireum Programming Language. - Robby; John Hatcliff (ISoLA, 2021)

Cyberassured Systems Engineering at Scale. - Darren D. Cofer; Isaac Amundson; Junaid Babar; David S. Hardin; Konrad Slind; Perry Alexander; John Hatcliff; Robby; Gerwin Klein; Corey Lewis; Eric Mercer; John Shackleton (IEEE Secur. Priv., 2022)

Awas: AADL information flow and error propagation analysis framework. - Hariharan Thiagarajan; John Hatcliff; Robby (Innov. Syst. Softw. Eng., 2022)

Model-driven development for the seL4 microkernel using the HAMR framework. - Jason Belt; John Hatcliff; Robby; John Shackleton; Jim Carciofini; Todd Carpenter; Eric Mercer; Isaac Amundson; Junaid Babar; Darren D. Cofer; David S. Hardin; Karl Hoech; et al. (J. Syst. Archit., 2023)

Logika: The Sireum Verification Framework. - Robby; John Hatcliff; Jason Belt (FMICS, 2024)

Integrated Contract-Based Unit and System Testing for Component-Based Systems. - John Hatcliff; Jason Belt; Robby; David S. Hardin (NFM, 2024)

Teaching with Logika: Conceiving and Constructing Correct Software. - Stefan Hallerstede; John Hatcliff; Robby (FMTea, 2024)

Proof Engineering in Logika: Synergistically Integrating Automated and Semi-automated Program Verification. - Stefan Hallerstede; Robby; John Hatcliff; Jason Belt; David S. Hardin (FMICS, 2025)

End-to-End Formal Methods Integrated Development with SysMLv2 Using HAMR. - John Hatcliff; Jason Belt; Robby; Clint McKenzie; Catalina Liang (FMICS, 2025)

Automated property-based testing from AADL component contracts. - John Hatcliff; Jason Belt; Robby; Jacob Legg; Danielle Stewart; Todd Carpenter (Int. J. Softw. Tools Technol. Transf., 2025)