English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Large language models have become increasingly effective in softwareengineering tasks such as code generation, debugging and repair. Languagemodels like ChatGPT can not only generate code, but also explain its innerworkings and in particular its correctness. This raises the question whether wecan utilize ChatGPT to support formal software verification.  In this paper, we take some first steps towards answering this question. Morespecifically, we investigate whether ChatGPT can generate loop invariants. Loopinvariant generation is a core task in software verification, and thegeneration of valid and useful invariants would likely help formal verifiers.To provide some first evidence on this hypothesis, we ask ChatGPT to annotate106 C programs with loop invariants. We check validity and usefulness of thegenerated invariants by passing them to two verifiers, Frama-C and CPAchecker.Our evaluation shows that ChatGPT is able to produce valid and usefulinvariants allowing Frama-C to verify tasks that it could not solve before.Based on our initial insights, we propose ways of combining ChatGPT (or largelanguage models in general) and software verifiers, and discuss currentlimitations and open issues.

Can ChatGPT support software verification?