UML Analysis Using State Diagrams. - Mohammad Alanazi; Jason Belt; David Gustafson (Software Engineering Research and Practice, 2006)

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

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)

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)

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)

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

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)

The Isolette System: Illustrating End-to-End Artifacts for Rigorous Model-Based Engineering. - John Hatcliff; Jason Belt (The Combined Power of Research, Education, and Dissemination, 2025)

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)