{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,7]],"date-time":"2026-01-07T05:46:16Z","timestamp":1767764776987,"version":"3.48.0"},"reference-count":27,"publisher":"MDPI AG","issue":"1","license":[{"start":{"date-parts":[[2026,1,2]],"date-time":"2026-01-02T00:00:00Z","timestamp":1767312000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100003170","name":"Knowledge Foundation","doi-asserted-by":"publisher","award":["20230054"],"award-info":[{"award-number":["20230054"]}],"id":[{"id":"10.13039\/501100003170","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Software"],"abstract":"<jats:p>Asserting program correctness is a longstanding challenge in software development that consumes lots of resources and manpower. It is often accomplished through software testing at various levels. One such level is unit testing, where the behaviour of individual components is tested. In this paper, we introduce the concept of test analysis, which instead of executing unit tests, analyses them to establish their outcome. This is line with previous approaches towards using formal methods for program verification; however, we introduce a middle layer called the test analysis framework, which allows for the introduction of new capabilities. We (briefly) formalize ordinary testing and test analysis to define the relation between the two. We introduce the notion of rich tests with a syntax and semantic instantiated for C. A prototype framework is implemented and extended to handle property-based stubbing and non-deterministic string variables. A few select examples are presented to demonstrate the capabilities of the framework.<\/jats:p>","DOI":"10.3390\/software5010002","type":"journal-article","created":{"date-parts":[[2026,1,2]],"date-time":"2026-01-02T09:56:23Z","timestamp":1767347783000},"page":"2","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["rUnit\u2014A Framework for Test Analysis of C Programs"],"prefix":"10.3390","volume":"5","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7965-248X","authenticated-orcid":false,"given":"Peter","family":"Backeman","sequence":"first","affiliation":[{"name":"School of Innovation, Design and EngineeringM\u00e4lardalen University, 721 23 V\u00e4ster\u00e5s, Sweden"}]}],"member":"1968","published-online":{"date-parts":[[2026,1,2]]},"reference":[{"key":"ref_1","doi-asserted-by":"crossref","first-page":"46","DOI":"10.1109\/MS.2017.3571582","article-title":"Software testing: The state of the practice","volume":"34","author":"Kassab","year":"2017","journal-title":"IEEE Softw."},{"key":"ref_2","doi-asserted-by":"crossref","first-page":"620836","DOI":"10.1155\/2010\/620836","article-title":"Software test automation in practice: Empirical observations","volume":"2010","author":"Kasurinen","year":"2010","journal-title":"Adv. Softw. Eng."},{"key":"ref_3","unstructured":"Khorikov, V. (2020). Unit Testing: Principles, Practices, and Patterns, Manning. [1st ed.]."},{"key":"ref_4","doi-asserted-by":"crossref","first-page":"859","DOI":"10.1145\/355604.361591","article-title":"The Humble Programmer","volume":"Volume 15","author":"Dijkstra","year":"1972","journal-title":"Communications of the ACM"},{"key":"ref_5","doi-asserted-by":"crossref","unstructured":"Beyer, D. (2024). State of the Art in Software Verification and Witness Validation: SV-COMP 2024. Tools and Algorithms for the Construction and Analysis of Systems; Lecture Notes in Computer Science, Springer Nature.","DOI":"10.1007\/978-3-031-57256-2_15"},{"key":"ref_6","doi-asserted-by":"crossref","unstructured":"Fischer, B., La Torre, S., Parlato, G., and Schrammel, P. (2022, January 10\u201314). CBMC-SSM: Bounded Model Checking of C Programs with Symbolic Shadow Memory. Proceedings of the ASE \u201922: 37th IEEE\/ACM International Conference on Automated Software Engineering, Rochester, MI, USA.","DOI":"10.1145\/3551349.3559523"},{"key":"ref_7","doi-asserted-by":"crossref","unstructured":"Khurshid, S., and Sen, K. (2011, January 27\u201330). Dynamic Race Detection with LLVM Compiler. Proceedings of the RV\u201911: Proceedings of the Second International Conference on Runtime Verification, San Francisco, CA, USA.","DOI":"10.1007\/978-3-642-29860-8"},{"key":"ref_8","doi-asserted-by":"crossref","unstructured":"Pecheur, C., and Dierkes, M. (2013). Study on the Barriers to the Industrial Adoption of Formal Methods. Formal Methods for Industrial Critical Systems, Springer.","DOI":"10.1007\/978-3-642-41010-9"},{"key":"ref_9","doi-asserted-by":"crossref","unstructured":"Chong, N., Cook, B., Kallas, K., Khazem, K., Monteiro, F.R., Schwartz-Narbonne, D., Tasiran, S., Tautschnig, M., and Tuttle, M.R. (2020\u201319, January 27). Code-Level Model Checking in the Software Development Workflow. Proceedings of the ICSE-SEIP \u201920: Proceedings of the ACM\/IEEE 42nd International Conference on Software Engineering: Software Engineering in Practice, Seoul, Republic of Korea.","DOI":"10.1145\/3377813.3381347"},{"key":"ref_10","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1134\/S0361768815010065","article-title":"Configurable toolset for static verification of operating systems kernel modules","volume":"41","author":"Zakharov","year":"2015","journal-title":"Program. Comput. Softw."},{"key":"ref_11","doi-asserted-by":"crossref","unstructured":"Ammann, P., and Offutt, J. (2008). Introduction to Software Testing, Cambridge University Press.","DOI":"10.1017\/CBO9780511809163"},{"key":"ref_12","unstructured":"Appel, F. (2015). Testing with JUnit: Master High-Quality Software Development Driven by Unit Tests, Packt Publishing."},{"key":"ref_13","unstructured":"Salunke, S. (2016). Junit with Examples, CreateSpace Independent Publishing Platform. [1st ed.]."},{"key":"ref_14","unstructured":"(2025, April 30). Google Test. Version 1.17.0, 2025. Available online: https:\/\/github.com\/google\/googletest."},{"key":"ref_15","first-page":"168","article-title":"A Tool for Checking ANSI-C Programs","volume":"Volume 2988","author":"Jensen","year":"2004","journal-title":"Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004)"},{"key":"ref_16","doi-asserted-by":"crossref","first-page":"1007","DOI":"10.1109\/TSE.2025.3537337","article-title":"How Do Developers Structure Unit Test Cases? An Empirical Analysis of the AAA Pattern in Open Source Projects","volume":"51","author":"Wei","year":"2025","journal-title":"IEEE Trans. Softw. Eng."},{"key":"ref_17","first-page":"230","article-title":"On Computable Numbers, with an Application to the {E}ntscheidungsproblem","volume":"2","author":"Turing","year":"1936","journal-title":"Proc. Lond. Math. Soc."},{"key":"ref_18","doi-asserted-by":"crossref","first-page":"60","DOI":"10.1145\/568438.568455","article-title":"Introduction to automata theory, languages, and computation","volume":"32","author":"Hopcroft","year":"2001","journal-title":"Acm Sigact News"},{"key":"ref_19","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1109\/MS.2013.43","article-title":"Testing or Formal Verification: DO-178C Alternatives and Industrial Experience","volume":"30","author":"Moy","year":"2013","journal-title":"IEEE Softw."},{"key":"ref_20","doi-asserted-by":"crossref","unstructured":"Souyris, J., Wiels, V., Delmas, D., and Delseny, H. (2009, January 2\u20136). Formal Verification of Avionics Software Products. Proceedings of the FM 2009: Formal Methods, Eindhoven, The Netherlands.","DOI":"10.1007\/978-3-642-05089-3_34"},{"key":"ref_21","doi-asserted-by":"crossref","unstructured":"Cook, B., Khazem, K., Kroening, D., Tasiran, S., Tautschnig, M., and Tuttle, M.R. (2018, January 14\u201317). Model checking boot code from AWS data centers. Proceedings of the CAV 2018, Oxford, UK.","DOI":"10.1007\/978-3-319-96142-2_28"},{"key":"ref_22","doi-asserted-by":"crossref","unstructured":"Gunter, E., and Peled, D. (2003). Unit Checking: Symbolic Model Checking for a Unit of Code. Verification: Theory and Practice: Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday, Springer.","DOI":"10.1007\/978-3-540-39910-0_24"},{"key":"ref_23","unstructured":"Amusuo, P.C., Patil, P.V., Cochell, O., Lievre, T.L., and Davis, J.C. (2024). Enabling Unit Proofing for Software Implementation Verification. arXiv."},{"key":"ref_24","unstructured":"Amusuo, P.C., Cochell, O., Lievre, T.L., Patil, P.V., Machiry, A., and Davis, J.C. (2025). Do Unit Proofs Work? An Empirical Study of Compositional Bounded Model Checking for Memory Safety Verification. arXiv."},{"key":"ref_25","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1145\/1095430.1081749","article-title":"Parameterized unit tests","volume":"30","author":"Tillmann","year":"2005","journal-title":"ACM SIGSOFT Softw. Eng. Notes"},{"key":"ref_26","doi-asserted-by":"crossref","unstructured":"Wu, Y., Deng, Q., and Zhang, W. (2023, January 22\u201324). A Strategy to Unwind Loops in Incremental Bounded Model Checking for Software. Proceedings of the AIBDF \u201923: Proceedings of the 2023 3rd Guangdong-Hong Kong-Macao Greater Bay Area Artificial Intelligence and Big Data Forum, Guangzhou, China.","DOI":"10.1145\/3660395.3660460"},{"key":"ref_27","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2499937.2499943","article-title":"On the Inference of Resource Usage Upper and Lower Bounds","volume":"14","author":"Albert","year":"2013","journal-title":"ACM Trans. Comput. Log."}],"container-title":["Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/2674-113X\/5\/1\/2\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,7]],"date-time":"2026-01-07T05:13:52Z","timestamp":1767762832000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/2674-113X\/5\/1\/2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,2]]},"references-count":27,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2026,3]]}},"alternative-id":["software5010002"],"URL":"https:\/\/doi.org\/10.3390\/software5010002","relation":{},"ISSN":["2674-113X"],"issn-type":[{"type":"electronic","value":"2674-113X"}],"subject":[],"published":{"date-parts":[[2026,1,2]]}}}