| Sireum/Topi LDP: a lightweight semi-decision procedure for optimizing symbolic execution-based analyses J Belt, Robby, X Deng Proceedings of the 7th joint meeting of the European software engineering …, 2009 | 23 | 2009 |
| HAMR: An AADL multi-platform code generation toolset J Hatcliff, J Belt, Robby, T Carpenter International Symposium on Leveraging Applications of Formal Methods, 274-295, 2021 | 22 | 2021 |
| Bakar kiasan: Flexible contract checking for critical systems using symbolic execution J Belt, J Hatcliff, Robby, P Chalin, D Hardin, X Deng NASA Formal Methods Symposium, 58-72, 2011 | 19 | 2011 |
| Model-driven development for the seL4 microkernel using the HAMR framework J Belt, J Hatcliff, J Shackleton, J Carciofini, T Carpenter, E Mercer, ... Journal of Systems Architecture 134, 102789, 2023 | 15 | 2023 |
| Explicating symbolic execution (xSymExe): An evidence-based verification framework J Hatcliff, P Chalin, J Belt 2013 35th International Conference on Software Engineering (ICSE), 222-231, 2013 | 11 | 2013 |
| Bakar Alir: supporting developers in construction of information flow contracts in SPARK H Thiagarajan, J Hatcliff, J Belt 2012 IEEE 12th International Working Conference on Source Code Analysis and …, 2012 | 8 | 2012 |
| Automated property-based testing from AADL component contracts J Hatcliff, J Belt, Robby, J Legg, D Stewart, T Carpenter International Conference on Formal Methods for Industrial Critical Systems …, 2023 | 5 | 2023 |
| An AADL Contract Language Supporting Integrated Model-and Code-Level Verification J Hatcliff, D Stewart, J Belt, A Schwerdfeger ACM SIGAda Ada Letters 42 (2), 45-54, 2023 | 5 | 2023 |
| Towards the formalization of SPARK 2014 semantics with explicit run-time checks using coq P Courtieu, MV Aponte, T Crolard, Z Zhang, F Robby, J Belt, J Hatcliff, ... Proceedings of the 2013 ACM SIGAda annual conference on High integrity …, 2013 | 5 | 2013 |
| A Unified Approach for Modeling, Developing, and Assuring Critical Systems J Hatcliff, BR Larson, J Belt, Robby, Y Zhang Leveraging Applications of Formal Methods, Verification and Validation …, 2018 | 4 | 2018 |
| Model-based development for high-assurance embedded systems Robby, J Hatcliff, J Belt Leveraging Applications of Formal Methods, Verification and Validation …, 2018 | 4 | 2018 |
| Automated Consistency Checking between UML State Charts and Sequence Diagram J Belt CIS, 2005 | 3 | 2005 |
| The isolette system: illustrating end-to-end artifacts for rigorous model-based engineering J Hatcliff, J Belt The Combined Power of Research, Education, and Dissemination: Essays …, 2024 | 2 | 2024 |
| Integrated contract-based unit and system testing for component-based systems J Hatcliff, J Belt, Robby, D Hardin NASA Formal Methods Symposium, 406-426, 2024 | 2 | 2024 |
| Efficient symbolic execution of value-based data structures for critical systems J Belt, Robby, P Chalin, J Hatcliff, X Deng NASA Formal Methods: 4th International Symposium, NFM 2012, Norfolk, VA, USA …, 2012 | 2 | 2012 |
| Logika: The Sireum Verification Framework Robby, J Hatcliff, J Belt International Conference on Formal Methods for Industrial Critical Systems …, 2024 | 1 | 2024 |
| Enhancing spark's contract checking facilities using symbolic execution J Belt, J Hatcliff, Robby, P Chalin, D Hardin, X Deng Proceedings of the 2011 ACM annual international conference on Special …, 2011 | 1 | 2011 |
| UML Analysis Using State Diagrams. M Alanazi, J Belt, D Gustafson Software Engineering Research and Practice, 569-576, 2006 | 1 | 2006 |
| Leading-edge Ada verification technologies: highly automated Ada contract checking using bakar kiasan J Belt, P Chalin, J Hatcliff, Robby ACM SIGAda Ada Letters 32 (3), 3-4, 2012 | | 2012 |
| Automated Consistency Checking Between UML State Diagrams and UML Sequence Diagrams JA Belt Kansas State University, 2006 | | 2006 |
