[FM-India] IARCS Verification Seminar Series -- Talk by Lucas Cordeiro on November 2, 1900 hrs IST

VSS IARCS vss.iarcs at gmail.com
Mon Nov 1 10:27:44 IST 2021


Dear all,

The next talk in the IARCS Verification Seminar Series will be given by
Lucas Cordeiro, a Reader in the Department of Computer Science at the
University of Manchester (UoM). The talk is scheduled on Tuesday, November
2, 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: Exploiting the SAT/SMT Revolution for Automated Software Verification

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

Abstract: In the last three decades, Boolean Satisfiability (SAT) solvers,
used as the backend of various verification engines, experienced a dramatic
performance revolution. SAT solvers can now check formulas that contain
millions of propositional variables. In Satisfiability Modulo Theories
(SMT) solvers, predicates from various theories are not encoded using
propositional variables as in SAT but remain in the problem formulation.
Thus, SMT solvers can be used as backends for solving the generated
verification conditions to cope with increasing software complexity. This
talk will overview automated software verification techniques that rely on
sophisticated SMT solvers built over efficient SAT solvers. I will discuss
challenges, problems, and recent advances to ensure safety and security in
embedded systems. I will describe novel algorithms that exploit
explicit-state and symbolic model checking for verifying single- and
multi-threaded software using SMT solvers. These algorithms were the first
to verify multi-threaded C/Posix software based on shared-memory
synchronization and communication symbolically. These algorithms are
implemented in software verification tools, now considered state-of-the-art
in the software testing and verification community, receiving 28 medals at
SV-COMP and Test-COMP. This achievement enabled industrial research
collaborations with Intel and Nokia. Software engineers applied these tools
to find real security vulnerabilities in large-scale software systems
(e.g., memory safety in firmware for Intel and arithmetic overflow in
telecommunication software for Nokia, neither of which had been found
before). Both were fixed after being confirmed business-critical.

Bio: Lucas Cordeiro is a Reader in the Department of Computer Science at
the University of Manchester (UoM), where he leads the Systems and Software
Security (S3) Research Group. Dr. Cordeiro is the Arm Centre of Excellence
Director at UoM; he also leads the Trusted Digital Systems cluster at the
Centre for Digital Trust and Society. He is also affiliated with the Formal
Methods Group at UoM. Dr. Cordeiro has implemented various tools used to
verify safety and security properties in significant industrial programs
written in Java, C/C++, and CUDA. Among those are ESBMC, an SMT-based model
checker for C/C++/Qt and CUDA, and JBMC, a SAT-based model checker for Java
bytecode. In the last ten years, he also won 28 awards from international
software verification and testing competitions held as part of ETAPS at
TACAS 2012-2021 and FASE 2020-2021. Dr. Cordeiro's industrial research
collaborators include Samsung, Nokia, Motorola, TP Vision, Intel, and ARM.
His tools have been applied to find real security vulnerabilities in
large-scale software systems. He has a proven track record of securing
research funding from Samsung, Nokia Institute of Technology, Motorola,
CAPES, CNPq, FAPEAM, British Council, EPSRC, and Royal Society. He leads
one large EPSRC project concerning verifiable and explainable secure AI. He
is Co-I on three others about software security and automated reasoning,
with a portfolio of approximately 5.4m GBP.


More information about the FMIndia mailing list