Seminar za računarstvo i primenjenu matematiku, 5. maj 2021.

Vanredni sastanak Seminara biće održan onlajn u sredu, 5. maja 2021. sa početkom u 20 časova.

Predavač: Philippa Gardner, Petar Maksimović

Naslov predavanja: GILLIAN: REAL-WORLD VERIFICATION OF JAVASCRIPT AND C

Apstrakt:
We will give a general introduction to Gillian, a platform for the development of symbolic-execution tools for many programming languages. Gillian currently supports three types of analysis: whole-program symbolic testing; full verification based on separation logic; and automatic compositional testing based on bi-abduction. It uses a core symbolic execution engine with strong mathematical foundations that unifies bug catching and verification. So far, we have instantiated Gillian to JavaScript and C. These instantiations have been used: to find bugs in the real-world data-structure libraries Buckets.js and Collections-C; to find bugs and prove bounded correctness results for a real-world jQuery-like library, cash; and to verify the deserialisation function of the AWS Encryption SDK messaging system, implemented in Javascript and C. We will focus on Gillian verification for this talk. This is a joint work of Philippa Gardner, Petar Maksimović, Jose Fragoso Santos, and Sacha Ayoun.

Publications:
Gillian, Part I: A Multi-language Platform for Symbolic Execution. Jose Fragoso Santos, Peter Maksimović, Sacha-Elie Ayoun, Philippa Gardner, PLDI'20.

Gillian, Part II: Real-World Verification for JavaScript and C. Petar Maksimović, Sacha-Élie Ayoun, José Fragoso Santos, Philippa Gardner. CAV'21.

Biografija predavača:
Philippa Gardner is a Professor in the Department of Computing at Imperial College London and a Fellow of the Royal Academy of Engineering. She currently holds a UK Research and Innovation Established Fellowship and directs the Research Institute on Verified Trustworthy Software Systems (VeTSS), funded by EPSRC and NCSC. Her research focusses on program testing and verification. In particular, her group is credited with bringing logical abstraction and logical atomicity to modern concurrent separation logics, developing trusted Coq-mechanised specifications of programming languages such as JavaScript and Web Assembly, and developing the Gillian platform for building symbolic-analysis tools for real-world programming languages such as JavaScript and C.

Petar Maksimović is a Research Fellow in the Department of Computing at Imperial College London. His expertise lies in the design and implementation of program analysis tools, including the JaVerT framework for the analysis of JavaScript programs, and the Gillian platform, which unifies testing and verification.

Detalji pristupa:
https://www.zoomgov.com/j/1611048580?pwd=clBqOVh3cGFUVGZENFgzN3p0YVBJdz09
Meeting ID: 161 104 8580
Passcode: 124006


 Ostavite vaš komentar 

Komentari(0)

Nažalost nije moguće ostaviti komentar.