IARCS Verification Seminar Series -- Talk by Shaz Qadeer on July 11 at 1900 hrs IST
Dear all, The next talk in the IARCS Verification Seminar Series will be given by Shaz Qadeer, an ACM Fellow, currently employed as a software engineer in the Core Infrastructure department at Meta. The talk is scheduled on Tuesday, July 11, at 1900 hrs IST (add to Google calendar <https://calendar.google.com/calendar/event?action=TEMPLATE&tmeid=MHF2OTJoMmlkcW1vdjYycWc5cmRzcGhmaTMgdnNzLmlhcmNzQG0&tmsrc=vss.iarcs%40gmail.com> ). The details of the talk can be found on our webpage ( https://fmindia.cmi.ac.in/vss/), and also appended to the body of this email. The Verification Seminar Series, an initiative by the Indian Association for Research in Computing Science (IARCS), is a monthly, online talk-series, broadly in the area of Formal Methods and Programming Languages, with applications in Verification and Synthesis. The aim of this talk-series is to provide a platform for Formal Methods researchers to interact regularly. In addition, we hope that it will make it easier for researchers to explore newer problems/areas and collaborate on them, and for younger researchers to start working in these areas. All are welcome to join. Best regards, Akash, Deepak, Madhukar, Srivathsan ============================================================= Title: Verification of Concurrent Programs with Civl Meeting Link: https://us02web.zoom.us/j/89164094870?pwd=eUFNRWp0bHYxRVpwVVNoVUdHU0djQT09 (Meeting ID: 891 6409 4870, Passcode: 082194) Abstract: The Civl verifier <https://civl-verifier.github.io/> introduces layered refinement, a new approach to the construction of verified concurrent programs and their proofs. This approach simplifies and scales (human and automated) reasoning by enabling a concurrent program to be represented and manipulated at multiple layers of abstraction. These abstraction layers are chained together via simple program transformations; each transformation is justified by a collection of automatically-checked verification conditions. Civl proofs are maintainable and reusable, specifically eliminating the need to write complex invariants on the low-level encoding of the concurrent program as a flat transition system. Civl has been used to construct verified low-level implementations of complex systems such as a concurrent garbage collector, a consensus protocol, and shared-memory data structures. Bio: Shaz Qadeer is an ACM Fellow. His research focuses on practical tools for the construction of verified concurrent and distributed systems. He is currently employed as a software engineer in the Core Infrastructure department at Meta.
participants (1)
-
VSS IARCS