Current formal analysis and verification methods often suffer scalability and/or precision issues. Moreover, applicability of these approaches in practice is frequently hindered by their inability to handle incomplete code (i.e., code fragments), while developers are reluctant to write verification harnesses for their code. At the same time, a need for further development of new verification techniques stems from constant arrival of new programming and specification languages and techniques, lately often involving AI-based methods.
