4 papers
Gradually Verifying Unfolding Expressions & Pure Functions
Hazel Torek, Long Tien Nguyen, Priyam Gupta +2
Unfolding expressions, which temporarily unfold a predicate to leverage its owned fields when evaluating a heap-dependent expression, and pure functions, which are heap-dependent f…
An Empirical Study of LLM-Generated Specifications for VeriFast
Wen Fan, Minh Tran, Sanya Dod +5
Static verification tools can assure industrial scale software, but require significant human labor to write specifications. This is particularly true of static verifiers based on…
Gradual Exact Logic: Unifying Hoare Logic and Incorrectness Logic via Gradual Verification
Conrad Zimmerman, Jenna DiVincenzo
Previously, gradual verification has been developed using overapproximating logics such as Hoare logic. We show that the static verification component of gradual verification is al…
Gradual Verification for Smart Contracts
Haojia Sun, Kunal Singh, Jan-Paul Ramos-Dávila +2
Blockchains facilitate secure resource transactions through smart contracts, yet these digital agreements are prone to vulnerabilities, particularly when interacting with external…