[FM-India] IARCS Verification Seminar Series -- Talk by Sorav Bansal on September 7, 1900 hrs IST

Madhavan Mukund madhavan at cmi.ac.in
Tue Aug 31 05:39:44 IST 2021

----- Forwarded message from VSS IARCS <vss.iarcs at gmail.com> -----

Date: Tue, 31 Aug 2021 00:32:35 +0530
From: VSS IARCS <vss.iarcs at gmail.com>
To: fmindia at cmi.ac.in
Subject: IARCS Verification Seminar Series -- Talk by Sorav Bansal on
  September 7, 1900 hrs IST

Dear all,

The next talk in the IARCS Verification Seminar Series will be given by
Sorav Bansal, an Associate Professor at IIT Delhi. The talk is scheduled on
Tuesday, September 7, at 1900 hrs IST. The details can be found on the
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,
Deepak, Madhukar, Rahul, Srivathsan


Title: Automatic BlackBox Equivalence Checking

Meeting Link:
(Meeting ID: 891 6409 4870, Passcode: 082194)

Abstract: Several important verification problems can be cast as
equivalence checking problems. A large number of these equivalence proofs
can be completed through bisimulation relation constructions. I will
present our recently proposed algorithm, called Counter, to automatically
compute equivalence (bisimulation) proofs across two programs, potentially
written in different syntaxes, without prior knowledge of the exact
differences between the two programs (blackbox). Counter has been
successfully used to validate translations of C programs to highly
optimized x86 assembly generated through modern compilers. Counter has also
been used to verify C library implementations. Through our experiments, we
have automatically generated proofs across complex compiler transformations
and found several bugs in popular open source programs and general-purpose
compilers. I will also briefly discuss the subtleties of checking
equivalence for LLVM programs. Finally I will outline our recent efforts at
automatic verification of C programs through the Counter algorithm.

This talk will be based on work published at APLAS 2017, HVC 2017, SAT
2018, PLDI 2020, and OOPSLA 2020. It will also include some of our ongoing

Bio: Sorav Bansal is an Associate Professor and Microsoft Chair Professor
at the CS department at IIT Delhi, and works in the areas of programming
languages and operating systems. His primary research interests involve
investigating superoptimization-based compiler design. His research papers
have appeared at PLDI, ASPLOS, SOSP, OSDI, OOPSLA, SAT, etc. Sorav obtained
his B.Tech. from IIT Delhi, and Ph.D. from Stanford University.

----- End forwarded message -----

More information about the FMIndia mailing list