Publications

Mayo, J.R., Morris Wright, K.V., Aytac, J.M., Smith, A.M., Armstrong, R.C., Hulette, G.C., Lober, R.R., & Lober, R.R. (2023). Demonstration of Model-Based Design for Digital Controller Using Formal Methods. 10.2172/2430067

Pollard, S.D., Armstrong, R.C., Bender, J., Hulette, G.C., Mahmood, R., Foulk, J.W., Rawlings, B.C., Aytac, J.M., & Aytac, J.M. (2022). Q: A Sound Verification Framework for Statecharts and their Implementations [Conference Paper]. 10.1145/3563822.3568014

Pollard, S.D., Armstrong, R.C., Aytac, J.M., Bender, J., Hulette, G.C., Mahmood, R., Foulk, J.W., Rawlings, B.C., & Rawlings, B.C. (2022). Q: A Sound Verification Framework for Statecharts and their Implementations [Conference Paper]. 10.1145/3563822.3568014

Kellison, A.E., Appel, A., Bindel, D., Thornquist, H.K., Hulette, G.C., & Hulette, G.C. (2022). Verification Toolchain for Floating-Point Programs [Conference Poster]. 10.2172/2004015

Hulette, G.C., Foulk, J.W., Armstrong, R.C., Snook, C., Hoang, T.S., Butler, M., & Butler, M. (2022). Formal verification and validation of run-to-completion style state charts using Event-B. Innovations in Systems and Software Engineering, 18(4). 10.1007/s11334-021-00416-4

Kellison, A.E., Tekriwal, M., Jeannin, J.B., Hulette, G.C., & Hulette, G.C. (2022). Towards Verified Rounding Error Analysis for Stationary Iterative Methods [Conference Paper]. Proceedings of Correctness 2022: 6th International Workshop on Software Correctness for HPC Applications, Held in conjunction with SC 2022: The International Conference for High Performance Computing, Networking, Storage and Analysis. 10.1109/Correctness56720.2022.00007

Pollard, S.D., Kellison, A., Bender, J., Thornquist, H.K., Hulette, G.C., & Hulette, G.C. (2021). Real(istic) Specifications of Software [Conference Paper]. https://www.osti.gov/biblio/2002959

Hulette, G.C., Bender, J., Pollard, S.D., Thornquist, H.K., Kellison, A., & Kellison, A. (2021). Formal Methods-based Certification Frameworks for Scientific Computing Applications [Conference Paper]. https://www.osti.gov/biblio/1897880

Foulk, J.W., Snook, C., Hoang, T.S., Armstrong, R.C., Hulette, G.C., Butler, M., & Butler, M. (2020). Refinement of Reactive Systems [Conference Poster]. https://www.osti.gov/biblio/1810037

Foulk, J.W., Snook, C., Hoang, T.S., Armstrong, R.C., Hulette, G.C., Butler, M., & Butler, M. (2020). Refinement and Verification of Responsive Control Systems [Conference Poster]. 10.1007/978-3-030-48077-6_23

Foulk, J.W., Snook, C., Hoang, T.S., Hulette, G.C., Armstrong, R.C., Butler, M., & Butler, M. (2020). Formal verification of run-to-completion style statecharts using event-b [Conference Poster]. Communications in Computer and Information Science. https://www.scopus.com/inward/record.uri?partnerID=HzOxMe3b&scp=85091515133&origin=inward

Hulette, G.C., Armstrong, R.C., & Armstrong, R.C. (2019). A Domain-Specific Language for High-Consequence Control Software. 10.2172/1592893

Armstrong, R.C., Evans, N., Hulette, G.C., Foulk, J.W., Aytac, J.M., Johnson-Freyd, P., Mayo, J.R., Punnoose, R.J., & Punnoose, R.J. (2019). Dishwashers of Armageddon: Verifying high consequence systems for Nuclear Weapons [Conference Poster]. https://www.osti.gov/biblio/1642936

Pollard, S.D., Johnson-Freyd, P., Aytac, J.M., Duckworth, T., Carson, M.J., Hulette, G.C., Harrison, C.B., & Harrison, C.B. (2019). Quameleon: A Lifter and Intermediate Language for Binary Analysis [Conference Poster]. https://www.osti.gov/biblio/1641972

Johnson-Freyd, P., Pollard, S.D., Duckworth, T., Carson, M.J., Hulette, G.C., Harrison, C.B., & Harrison, C.B. (2019). Quameleon: A Lifter and Intermediate Language for Binary Analysis [Conference Poster]. https://www.osti.gov/biblio/1641001

Mayo, J.R., Armstrong, R.C., Hulette, G.C., Salloum, M., Smith, A.M., & Smith, A.M. (2018). Robust digital computation in the physical world. Cyber-Physical Systems Security. 10.1007/978-3-319-98935-8_1

Armstrong, R.C., Foulk, J.W., Hulette, G.C., Mayo, J.R., Michnovicz, J., Aytac, J.M., Johnson-Freyd, P., Punnoose, R.J., Smith, A.M., & Smith, A.M. (2017). Tools for Simple Yet Very High Consequence Controls [Presentation]. https://www.osti.gov/biblio/1513847

Armstrong, R.C., Aytac, J.M., Hulette, G.C., Mayo, J.R., Foulk, J.W., & Foulk, J.W. (2017). Compiling Statecharts into Why3 [Presentation]. https://www.osti.gov/biblio/1457972

Foulk, J.W., Hulette, G.C., Mayo, J.R., Foulk, J.W., & Foulk, J.W. (2016). Formal Verification of High-Consequence Digital Controls [Conference Poster]. https://www.osti.gov/biblio/1806530

Hulette, G.C., Johnson-Freyd, P., Ariola, Z., & Ariola, Z. (2016). Verification by way of refinement: a case study in the use of Coq and TLA in the design of a safety critical system [Conference Poster]. https://www.osti.gov/biblio/1368799

Johnson-Freyd, P., Hulette, G.C., Ariola, Z.M., & Ariola, Z.M. (2016). Verification by way of refinement: A case study in the use of coq and TLA in the design of a safety critical system [Conference Poster]. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). https://doi.org/10.1007/978-3-319-45943-1_14

Mayo, J.R., Armstrong, R.C., Hulette, G.C., & Hulette, G.C. (2016). Leveraging abstraction to establish out-of-nominal safety properties [Conference Poster]. Communications in Computer and Information Science. 10.1007/978-3-319-29510-7_10

Mayo, J.R., Armstrong, R.C., Hulette, G.C., & Hulette, G.C. (2015). Leveraging Abstraction to Establish Out-of-Nominal Safety Properties [Conference Poster]. 10.1007/978-3-319-29510-7_10

Mayo, J.R., Armstrong, R.C., Hulette, G.C., & Hulette, G.C. (2015). Digital system robustness via design constraints: The lesson of formal methods [Conference Poster]. 9th Annual IEEE International Systems Conference, SysCon 2015 - Proceedings. https://www.scopus.com/inward/record.uri?partnerID=HzOxMe3b&scp=84941313075&origin=inward

Mayo, J.R., Armstrong, R.C., Hulette, G.C., & Hulette, G.C. (2014). Digital System Robustness via Design Constraints: The Lesson of Formal Methods [Conference Poster]. 10.1109/SYSCON.2015.7116737