Congratulations to Petar, Jose, Sacha and Philippa, whose paper and artifact has been accepted to CAV 2021, the [33rd International Conference on Computer-Aided Verification.](http://i-cav.org/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.](http://i-cav.org/2021/)
In their paper, Gillian, Part II: Real-World Verification for JavaScript and C, they introduce verification based on separation logic to [Gillian](https://vtss.doc.ic.ac.uk/research/gillian.html), and their methodology for constructing compositional memory models for Gillian. They also verify the JavaScript and C implementations of the [AWS Encryption SDK](https://docs.aws.amazon.com/encryption-sdk/latest/developer-guide/introduction.html) message header deserialisation module, where they found two bugs in the JavaScript and three bugs in the C implementation.
