Paper accepted at CAV 2021
Congratulations to Petar, Jose, Sacha and Philippa, whose paper and artifact have been accepted to CAV 2021, the 33rd International Conference on Computer-Aided Verification.
In their paper, Gillian, Part II: Real-World Verification for JavaScript and C, they introduce verification based on separation logic to Gillian, and their methodology for constructing compositional memory models for Gillian. They also verify the JavaScript and C implementations of the AWS Encryption SDK message header deserialisation module, where they found two bugs in the JavaScript and three bugs in the C implementation.
CAV is dedicated to the advancement of the theory and practice of computer-aided formal analysis methods for hardware and software systems and will be held online this year.