[FM-India] IARCS Verification Seminar Series -- Talk by Peter Schrammel on March 1, 1900 hrs IST

[VSS IARCS]

Dear all,

The next talk in the IARCS Verification Seminar Series will be given by
Peter Schrammel, CTO and co-founder of Diffblue, and also an Assistant
Professor of Computer Science at the University of Sussex. The talk is
scheduled on Tuesday, March 1, at 1900 hrs IST (add to calendar
<https://fmindia.cmi.ac.in/vss/cal/vss-1Mar2022.ics>:
https://fmindia.cmi.ac.in/vss/cal/vss-1Mar2022.ics).

The details of the talk 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: Parallel Bug-finding in Concurrent Programs via Reduced Interleaving
Instances

Meeting Link:
https://us02web.zoom.us/j/89164094870?pwd=eUFNRWp0bHYxRVpwVVNoVUdHU0djQT09
(Meeting ID: 891 6409 4870, Passcode: 082194)

Abstract: Concurrency poses a major challenge for program verification, but
it can also offer an opportunity to scale when subproblems can be analysed
in parallel. We exploit this opportunity here and use a parametrizable
code-to-code translation to generate a set of simpler program instances,
each capturing a reduced set of the original program's interleavings. These
instances can then be checked independently in parallel. Our approach does
not depend on the tool that is chosen for the final analysis, is compatible
with weak memory models, and amplifies the effectiveness of existing tools,
making them find bugs faster and with fewer resources. We use Lazy-CSeq as
an off-the-shelf final verifier to demonstrate that our approach is able,
already with a small number of cores, to find bugs in the hardest known
concurrency benchmarks in a matter of minutes, whereas other dynamic and
static tools fail to do so in hours.

Bio: Peter Schrammel is CTO and co-founder of Diffblue. He is also an
Assistant Professor of Computer Science at the University of Sussex. His
research interests lie in formal methods for building dependable systems
and understanding complex systems. In particular, his interests include
program analysis algorithms combining abstract interpretation and decision
procedures, acceleration and strategy iteration methods for efficient and
precise invariant inference, incremental solving and abstraction
refinement, and verification and testing of cyber-physical systems.