Assessing Postcondition Completeness in Auto-Generated Function Contracts for Software Verification
Resumo
The precision of specifications plays a crucial role in system verification, with correctness and completeness being complementary properties required for soundness. Previous approaches for automated software verification focused mainly on evaluating correctness, overlooking or only partially addressing the specification completeness. Recent work has renewed interest in completeness evaluation, but existing approaches remain critically dependent on test suites, effectively shifting the challenge of assessing the coverage of the specification to the coverage of the tests. To overcome this limitation, we introduce a novel method for checking postcondition completeness that can evaluate whether a specification is the Strongest Postcondition, requiring only the candidate specification for a deterministic program. To assess its feasibility, we evaluated our completeness check across representative LLM-based specification generation approaches, demonstrating its effectiveness, reliability, and potential for automated verification.
Palavras-chave:
Specification Completeness, Strongest Postcondition, Specification Coverage, Program Verification, Formal Specification, Large Language Models
Referências
Samia Alblwi, Amani Ayad, and Ali Mili. 2024. Mutation Coverage is not Strongly Correlated with Mutation Coverage. In Proceedings of the 5th ACM/IEEE International Conference on Automation of Software Test (AST 2024) (Lisbon, Portugal) (AST ’24). Association for Computing Machinery, New York, NY, USA, 1–11. DOI: 10.1145/3644032.3644442
Paul E. Ammann and Paul E. Black. 2000. A Specification-Based Coverage Metric To Evaluate Test Sets. International Journal of Reliability, Quality and Safety Engineering 8 (11 2000). DOI: 10.1142/S0218539301000530
Samuel Amorim, Leonardo Fernandes, Márcio Ribeiro, Rohit Gheyi, Márcio Eduardo Delamaro, Marcio Guimarães, and André Santos. 2024. Reducing manual efforts in equivalence analysis in mutation testing. Journal of Software Engineering Research and Development 13, 3 (2024), 1–17.
Dimitrios Athanasiou, Ariadi Nugroho, Joost Visser, and Andy Zaidman. 2014. Test Code Quality and Its Relation to Issue Handling Performance. IEEE Transactions on Software Engineering 40, 11 (2014), 1100–1125. DOI: 10.1109/TSE.2014.2342227
Ragib Shahariar Ayon and Shibbir Ahmed. 2026. AutoReSpec: A Framework for Generating Specification using Large Language Models. arXiv:2604.03758 [cs.SE] [link]
Nick Benton. 2004. Simple relational correctness proofs for static analyses and program transformations. SIGPLAN Not. 39, 1 (Jan. 2004), 14–25. DOI: 10.1145/982962.964003
Daniel M Berry. 2002. Formal methods: the very idea: Some thoughts about why they work when they work. Science of Computer Programming 42, 1 (2002), 11–27. DOI: 10.1016/S0167-6423(01)00026-0, Special Issue on Engineering Automation for Computer Based Systems.
Allan Blanchard. 2020. Introduction to C program proof with Frama-C and its WP plugin. [link]
Claudinei Brito, Vinicius H. S. Durelli, Rafael S. Durelli, Simone R. S. de Souza, Auri M. R. Vincenzi, and Marcio Eduardo Delamaro. 2020. A preliminary investigation into using machine learning algorithms to identify minimal and equivalent mutants. In 2020 IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW). IEEE, 304–313.
Lea Salome Brugger, Xavier Denis, and Peter Müller. 2026. Toward Practical Deductive Verification: Insights from a Qualitative Survey in Industry and Academia. arXiv:2510.20514 [cs.SE] [link]
José Campos, Yan Ge, Nasser Albunian, Gordon Fraser, Marcelo Eler, and Andrea Arcuri. 2018. An empirical evaluation of evolutionary algorithms for unit test suite generation. Information and Software Technology 104 (2018), 207–235.
David R. Cok. 2025. User guide to specification and verification with the Java Modeling Language and OpenJML. DRAFT September 27, 2025. [link]
David R. Cok, Gary T. Leavens, and Mattias Ulbrich. 2025. Java Modeling Language (JML). Reference Manual. 2ed. DRAFT September 27, 2025. [link]
Edsger W. Dijkstra and Carel S. Schölten. 1990. The strongest postcondition. Springer New York, New York, NY, 209–215. DOI: 10.1007/978-1-4612-3228-5_12
Arnaud Ebalard, Patricia Mouy, and Ryad Benadjila. 2019. Journey to a RTE-free X.509 parser. In Symposium sur la sécurité des technologies de l’information et des communications (SSTIC). 29–49. [link]
Madeline Endres, Sarah Fakhoury, Saikat Chakraborty, and Shuvendu K. Lahiri. 2024. Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions? Proc. ACM Softw. Eng. 1, FSE, Article 84 (July 2024), 24 pages. DOI: 10.1145/3660791
Michael D. Ernst, Jeff H. Perkins, Philip J. Guo, Stephen McCamant, Carlos Pacheco, Matthew S. Tschantz, and Chen Xiao. 2007. The Daikon system for dynamic detection of likely invariants. Science of Computer Programming 69, 1 (2007), 35–45. DOI: 10.1016/j.scico.2007.01.015, Special issue on Experimental Software and Toolkits.
Cormac Flanagan and K. Rustan M. Leino. 2001. Houdini, an Annotation Assistant for ESC/Java. In FME 2001: Formal Methods for Increasing Software Productivity, José Nuno Oliveira and Pamela Zave (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 500–517.
Jens Gerlach. 2025. ACSL by Example: Version 32.0.0 for Frama-C 32.0 (Germanium). Fraunhofer FOKUS (2025). [link]
Mike Gordon. 2016. Background reading on Hoare Logic. Learning guide / lecture notes. University of Cambridge, Computer Laboratory. MJCG February 2, 2016, available at url [link].
Dalton N. Jorge, Patrícia D. L. Machado, Everton L. G. Alves, and Wilkerson L. Andrade. 2018. Integrating requirements specification and model-based testing in agile development. In 2018 IEEE 26th International Requirements Engineering Conference (RE). IEEE, 336–346.
Samuel J. Kaufman, Ryan Featherman, Justin Alvin, Bob Kurtz, Paul Ammann, and René Just. 2022. Prioritizing mutants to guide mutation testing. In Proceedings of the 44th International Conference on Software Engineering (Pittsburgh, Pennsylvania) (ICSE ’22). Association for Computing Machinery, New York, NY, USA, 1743–1754. DOI: 10.1145/3510003.3510187
Benjamin Kushigian, Samuel J. Kaufman, Ryan Featherman, Hannah Potter, Ardi Madadi, and René Just. 2024. Equivalent Mutants in the Wild: Identifying and Efficiently Suppressing Equivalent Mutants for Java Programs. In Proceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis (Vienna, Austria) (ISSTA 2024). Association for Computing Machinery, New York, NY, USA, 654–665. DOI: 10.1145/3650212.3680310
Thanh Le-Cong, Bach Le, and Toby Murray. 2025. Can LLMs Reason About Program Semantics? A Comprehensive Evaluation of LLMs on Formal Specification Inference. In Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers),Wanxiang Che, Joyce Nabende, Ekaterina Shutova, and Mohammad Taher Pilehvar (Eds.). Association for Computational Linguistics, Vienna, Austria, 21991–22014. DOI: 10.18653/v1/2025.acllong.1068
Chang Liu. 2019. fluency03 LeetCode Java problems GitHub repository. [link]
Lezhi Ma, Shangqing Liu, Yi Li, Xiaofei Xie, and Lei Bu. 2025. Github repository artifact - SpecGen: Automated Generation of Formal Program Specifications via Large Language Models. [link]
Lezhi Ma, Shangqing Liu, Yi Li, Xiaofei Xie, and Lei Bu. 2025. SpecGen: Automated Generation of Formal Program Specifications via Large Language Models. In 2025 IEEE/ACM 47th International Conference on Software Engineering (ICSE). 16–28. DOI: 10.1109/ICSE55347.2025.00129
Md Rakib Hossain Misu, Iris Ma, and Cristina V. Lopes. 2026. VeriAct: Beyond Verifiability – Agentic Synthesis of Correct and Complete Formal Specifications. arXiv:2604.00280 [cs.SE] [link]
Facundo Molina, Marcelo d’Amorim, and Nazareno Aguirre. 2022. Fuzzing class specifications. In Proceedings of the 44th International Conference on Software Engineering (Pittsburgh, Pennsylvania) (ICSE ’22). Association for Computing Machinery, New York, NY, USA, 1008–1020. DOI: 10.1145/3510003.3510120
Rashmi Mudduluru, Jason Waataja, Suzanne Millstein, and Michael Ernst. 2021. Verifying Determinism in Sequential Programs. In 2021 IEEE/ACM 43rd International Conference on Software Engineering (ICSE). 37–49. DOI: 10.1109/ICSE43902.2021.00017
OpenAI. 2025. OpenAI Models — Model Reference Documentation. [link]. Accessed: 2025-11-29.
OpenJML. 2026. OpenJML Frame Conditions Tutorial. [link]. Accessed: 2026-02-15.
Cedric Richter and Heike Wehrheim. 2025. Beyond Postconditions: Can Large Language Models infer Formal Contracts for Automatic Software Verification? arXiv:2510.12702 [cs.SE] [link]
John L. Singleton, Gary T. Leavens, Hridesh Rajan, and David Cok. 2018. An algorithm and tool to infer practical postconditions. In Proceedings of the 40th International Conference on Software Engineering: Companion Proceedings (Gothenburg, Sweden) (ICSE ’18). Association for Computing Machinery, New York, NY, USA, 313–314. DOI: 10.1145/3183440.3194986
Chuyue Sun, Ying Sheng, Oded Padon, and Clark Barrett. 2024. Clover: Closed-Loop Verifiable Code Generation. In AI Verification, Guy Avni, Mirco Giacobbe, Taylor T. Johnson, Guy Katz, Anna Lukina, Nina Narodytska, and Christian Schilling (Eds.). Springer Nature Switzerland, Cham, 134–155.
Zhao Tian, Junjie Chen, Qihao Zhu, Junjie Yang, and Lingming Zhang. 2023. Learning to Construct Better Mutation Faults. In Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering (Rochester, MI, USA) (ASE ’22). Association for Computing Machinery, New York, NY, USA, Article 64, 13 pages. DOI: 10.1145/3551349.3556949
Norbert Tihanyi, Tamas Bisztray, Mohamed Amine Ferrag, Ridhi Jain, and Lucas C. Cordeiro. 2025. How secure is AI-generated code: a large-scale comparison of large language models. Empirical Software Engineering 30, 47 (2025). DOI: 10.1007/s10664-024-10590-1
Cheng Wen, Jialun Cao, Jie Su, Zhiwu Xu, Shengchao Qin, Mengda He, Haokun Li, Shing-Chi Cheung, and Cong Tian. 2024. Enchanting Program Specification Synthesis by Large Language Models Using Static Analysis and Program Verification. In Computer Aided Verification, Arie Gurfinkel and Vijay Ganesh (Eds.). Springer Nature Switzerland, Cham, 302–328.
Guangyuan Wu, Weining Cao, Yuan Yao, Hengfeng Wei, Taolue Chen, and Xiaoxing Ma. 2024. LLM Meets Bounded Model Checking: Neuro-symbolic Loop Invariant Inference. In Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering (Sacramento, CA, USA) (ASE ’24). Association for Computing Machinery, New York, NY, USA, 406–417. DOI: 10.1145/3691620.3695014
Yiheng Xiong, Mengqian Xu, Ting Su, Jingling Sun, Jue Wang, HeWen, Geguang Pu, Jifeng He, and Zhendong Su. 2023. An Empirical Study of Functional Bugs in Android Apps. In Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis (Seattle, WA, USA) (ISSTA 2023). Association for Computing Machinery, New York, NY, USA, 1319–1331. DOI: 10.1145/3597926.3598138
Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu K. Lahiri, Jacob R. Lorch, Shuai Lu, Fan Yang, Ziqiao Zhou, and Shan Lu. 2025. Autoverus: Automated Proof Generation for Rust Code. Proceedings of the ACM on Programming Languages 9, OOPSLA2 (2025).
Jianan Yao, Gabriel Ryan, Justin Wong, Suman Jana, and Ronghui Gu. 2020. Learning nonlinear loop invariants with gated continuous logic networks. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. 106–120.
Paul E. Ammann and Paul E. Black. 2000. A Specification-Based Coverage Metric To Evaluate Test Sets. International Journal of Reliability, Quality and Safety Engineering 8 (11 2000). DOI: 10.1142/S0218539301000530
Samuel Amorim, Leonardo Fernandes, Márcio Ribeiro, Rohit Gheyi, Márcio Eduardo Delamaro, Marcio Guimarães, and André Santos. 2024. Reducing manual efforts in equivalence analysis in mutation testing. Journal of Software Engineering Research and Development 13, 3 (2024), 1–17.
Dimitrios Athanasiou, Ariadi Nugroho, Joost Visser, and Andy Zaidman. 2014. Test Code Quality and Its Relation to Issue Handling Performance. IEEE Transactions on Software Engineering 40, 11 (2014), 1100–1125. DOI: 10.1109/TSE.2014.2342227
Ragib Shahariar Ayon and Shibbir Ahmed. 2026. AutoReSpec: A Framework for Generating Specification using Large Language Models. arXiv:2604.03758 [cs.SE] [link]
Nick Benton. 2004. Simple relational correctness proofs for static analyses and program transformations. SIGPLAN Not. 39, 1 (Jan. 2004), 14–25. DOI: 10.1145/982962.964003
Daniel M Berry. 2002. Formal methods: the very idea: Some thoughts about why they work when they work. Science of Computer Programming 42, 1 (2002), 11–27. DOI: 10.1016/S0167-6423(01)00026-0, Special Issue on Engineering Automation for Computer Based Systems.
Allan Blanchard. 2020. Introduction to C program proof with Frama-C and its WP plugin. [link]
Claudinei Brito, Vinicius H. S. Durelli, Rafael S. Durelli, Simone R. S. de Souza, Auri M. R. Vincenzi, and Marcio Eduardo Delamaro. 2020. A preliminary investigation into using machine learning algorithms to identify minimal and equivalent mutants. In 2020 IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW). IEEE, 304–313.
Lea Salome Brugger, Xavier Denis, and Peter Müller. 2026. Toward Practical Deductive Verification: Insights from a Qualitative Survey in Industry and Academia. arXiv:2510.20514 [cs.SE] [link]
José Campos, Yan Ge, Nasser Albunian, Gordon Fraser, Marcelo Eler, and Andrea Arcuri. 2018. An empirical evaluation of evolutionary algorithms for unit test suite generation. Information and Software Technology 104 (2018), 207–235.
David R. Cok. 2025. User guide to specification and verification with the Java Modeling Language and OpenJML. DRAFT September 27, 2025. [link]
David R. Cok, Gary T. Leavens, and Mattias Ulbrich. 2025. Java Modeling Language (JML). Reference Manual. 2ed. DRAFT September 27, 2025. [link]
Edsger W. Dijkstra and Carel S. Schölten. 1990. The strongest postcondition. Springer New York, New York, NY, 209–215. DOI: 10.1007/978-1-4612-3228-5_12
Arnaud Ebalard, Patricia Mouy, and Ryad Benadjila. 2019. Journey to a RTE-free X.509 parser. In Symposium sur la sécurité des technologies de l’information et des communications (SSTIC). 29–49. [link]
Madeline Endres, Sarah Fakhoury, Saikat Chakraborty, and Shuvendu K. Lahiri. 2024. Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions? Proc. ACM Softw. Eng. 1, FSE, Article 84 (July 2024), 24 pages. DOI: 10.1145/3660791
Michael D. Ernst, Jeff H. Perkins, Philip J. Guo, Stephen McCamant, Carlos Pacheco, Matthew S. Tschantz, and Chen Xiao. 2007. The Daikon system for dynamic detection of likely invariants. Science of Computer Programming 69, 1 (2007), 35–45. DOI: 10.1016/j.scico.2007.01.015, Special issue on Experimental Software and Toolkits.
Cormac Flanagan and K. Rustan M. Leino. 2001. Houdini, an Annotation Assistant for ESC/Java. In FME 2001: Formal Methods for Increasing Software Productivity, José Nuno Oliveira and Pamela Zave (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 500–517.
Jens Gerlach. 2025. ACSL by Example: Version 32.0.0 for Frama-C 32.0 (Germanium). Fraunhofer FOKUS (2025). [link]
Mike Gordon. 2016. Background reading on Hoare Logic. Learning guide / lecture notes. University of Cambridge, Computer Laboratory. MJCG February 2, 2016, available at url [link].
Dalton N. Jorge, Patrícia D. L. Machado, Everton L. G. Alves, and Wilkerson L. Andrade. 2018. Integrating requirements specification and model-based testing in agile development. In 2018 IEEE 26th International Requirements Engineering Conference (RE). IEEE, 336–346.
Samuel J. Kaufman, Ryan Featherman, Justin Alvin, Bob Kurtz, Paul Ammann, and René Just. 2022. Prioritizing mutants to guide mutation testing. In Proceedings of the 44th International Conference on Software Engineering (Pittsburgh, Pennsylvania) (ICSE ’22). Association for Computing Machinery, New York, NY, USA, 1743–1754. DOI: 10.1145/3510003.3510187
Benjamin Kushigian, Samuel J. Kaufman, Ryan Featherman, Hannah Potter, Ardi Madadi, and René Just. 2024. Equivalent Mutants in the Wild: Identifying and Efficiently Suppressing Equivalent Mutants for Java Programs. In Proceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis (Vienna, Austria) (ISSTA 2024). Association for Computing Machinery, New York, NY, USA, 654–665. DOI: 10.1145/3650212.3680310
Thanh Le-Cong, Bach Le, and Toby Murray. 2025. Can LLMs Reason About Program Semantics? A Comprehensive Evaluation of LLMs on Formal Specification Inference. In Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers),Wanxiang Che, Joyce Nabende, Ekaterina Shutova, and Mohammad Taher Pilehvar (Eds.). Association for Computational Linguistics, Vienna, Austria, 21991–22014. DOI: 10.18653/v1/2025.acllong.1068
Chang Liu. 2019. fluency03 LeetCode Java problems GitHub repository. [link]
Lezhi Ma, Shangqing Liu, Yi Li, Xiaofei Xie, and Lei Bu. 2025. Github repository artifact - SpecGen: Automated Generation of Formal Program Specifications via Large Language Models. [link]
Lezhi Ma, Shangqing Liu, Yi Li, Xiaofei Xie, and Lei Bu. 2025. SpecGen: Automated Generation of Formal Program Specifications via Large Language Models. In 2025 IEEE/ACM 47th International Conference on Software Engineering (ICSE). 16–28. DOI: 10.1109/ICSE55347.2025.00129
Md Rakib Hossain Misu, Iris Ma, and Cristina V. Lopes. 2026. VeriAct: Beyond Verifiability – Agentic Synthesis of Correct and Complete Formal Specifications. arXiv:2604.00280 [cs.SE] [link]
Facundo Molina, Marcelo d’Amorim, and Nazareno Aguirre. 2022. Fuzzing class specifications. In Proceedings of the 44th International Conference on Software Engineering (Pittsburgh, Pennsylvania) (ICSE ’22). Association for Computing Machinery, New York, NY, USA, 1008–1020. DOI: 10.1145/3510003.3510120
Rashmi Mudduluru, Jason Waataja, Suzanne Millstein, and Michael Ernst. 2021. Verifying Determinism in Sequential Programs. In 2021 IEEE/ACM 43rd International Conference on Software Engineering (ICSE). 37–49. DOI: 10.1109/ICSE43902.2021.00017
OpenAI. 2025. OpenAI Models — Model Reference Documentation. [link]. Accessed: 2025-11-29.
OpenJML. 2026. OpenJML Frame Conditions Tutorial. [link]. Accessed: 2026-02-15.
Cedric Richter and Heike Wehrheim. 2025. Beyond Postconditions: Can Large Language Models infer Formal Contracts for Automatic Software Verification? arXiv:2510.12702 [cs.SE] [link]
John L. Singleton, Gary T. Leavens, Hridesh Rajan, and David Cok. 2018. An algorithm and tool to infer practical postconditions. In Proceedings of the 40th International Conference on Software Engineering: Companion Proceedings (Gothenburg, Sweden) (ICSE ’18). Association for Computing Machinery, New York, NY, USA, 313–314. DOI: 10.1145/3183440.3194986
Chuyue Sun, Ying Sheng, Oded Padon, and Clark Barrett. 2024. Clover: Closed-Loop Verifiable Code Generation. In AI Verification, Guy Avni, Mirco Giacobbe, Taylor T. Johnson, Guy Katz, Anna Lukina, Nina Narodytska, and Christian Schilling (Eds.). Springer Nature Switzerland, Cham, 134–155.
Zhao Tian, Junjie Chen, Qihao Zhu, Junjie Yang, and Lingming Zhang. 2023. Learning to Construct Better Mutation Faults. In Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering (Rochester, MI, USA) (ASE ’22). Association for Computing Machinery, New York, NY, USA, Article 64, 13 pages. DOI: 10.1145/3551349.3556949
Norbert Tihanyi, Tamas Bisztray, Mohamed Amine Ferrag, Ridhi Jain, and Lucas C. Cordeiro. 2025. How secure is AI-generated code: a large-scale comparison of large language models. Empirical Software Engineering 30, 47 (2025). DOI: 10.1007/s10664-024-10590-1
Cheng Wen, Jialun Cao, Jie Su, Zhiwu Xu, Shengchao Qin, Mengda He, Haokun Li, Shing-Chi Cheung, and Cong Tian. 2024. Enchanting Program Specification Synthesis by Large Language Models Using Static Analysis and Program Verification. In Computer Aided Verification, Arie Gurfinkel and Vijay Ganesh (Eds.). Springer Nature Switzerland, Cham, 302–328.
Guangyuan Wu, Weining Cao, Yuan Yao, Hengfeng Wei, Taolue Chen, and Xiaoxing Ma. 2024. LLM Meets Bounded Model Checking: Neuro-symbolic Loop Invariant Inference. In Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering (Sacramento, CA, USA) (ASE ’24). Association for Computing Machinery, New York, NY, USA, 406–417. DOI: 10.1145/3691620.3695014
Yiheng Xiong, Mengqian Xu, Ting Su, Jingling Sun, Jue Wang, HeWen, Geguang Pu, Jifeng He, and Zhendong Su. 2023. An Empirical Study of Functional Bugs in Android Apps. In Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis (Seattle, WA, USA) (ISSTA 2023). Association for Computing Machinery, New York, NY, USA, 1319–1331. DOI: 10.1145/3597926.3598138
Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu K. Lahiri, Jacob R. Lorch, Shuai Lu, Fan Yang, Ziqiao Zhou, and Shan Lu. 2025. Autoverus: Automated Proof Generation for Rust Code. Proceedings of the ACM on Programming Languages 9, OOPSLA2 (2025).
Jianan Yao, Gabriel Ryan, Justin Wong, Suman Jana, and Ronghui Gu. 2020. Learning nonlinear loop invariants with gated continuous logic networks. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. 106–120.
Publicado
08/09/2026
Como Citar
SILVEIRA, Caio Vinícius Pereira; FERREIRA, Mateus Felipe Tymburibá.
Assessing Postcondition Completeness in Auto-Generated Function Contracts for Software Verification. In: SIMPÓSIO BRASILEIRO DE TESTES DE SOFTWARE SISTEMÁTICO E AUTOMATIZADO (SAST), 11. , 2026, São Paulo/SP.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2026
.
p. 19-28.
DOI: https://doi.org/10.5753/sast.2026.30683.
