[FM-India]IARCS Verification Seminar Series -- Talk by Mahesh Viswanathan on Oct. 4 at 1900 hrs IST

Dear all, The next talk in the IARCS Verification Seminar Series will be given by Mahesh Viswanathan, a faculty member at the University of Illinois at Urbana-Champaign. The talk is scheduled on Tuesday, October 4, at 1900 hrs IST (add to Google calendar <https://calendar.google.com/event?action=TEMPLATE&tmeid=NmI5c2FkdXNhMGs0YnM0OGo3ZGNiN3UxbmwgdnNzLmlhcmNzQG0&tmsrc=vss.iarcs%40gmail.com> ). 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: On Linear Time Decidability of Differential Privacy for Programs with Unbounded Inputs Meeting Link: https://us02web.zoom.us/j/89164094870?pwd=eUFNRWp0bHYxRVpwVVNoVUdHU0djQT09 (Meeting ID: 891 6409 4870, Passcode: 082194) Abstract: We introduce an automata model for describing interesting classes of differential privacy mechanisms/algorithms that include known mechanisms from the literature. These automata can model algorithms whose inputs can be an unbounded sequence of real-valued query answers. We consider the problem of checking whether there exists a constant $d$ such that the algorithm described by these automata are $d\epsilon$-differentially private for all positive values of the privacy budget parameter $\epsilon$. We show that this problem can be decided in time linear in the automaton's size by identifying a necessary and sufficient condition on the underlying graph of the automaton. This paper's results are the first decidability results known for algorithms with an unbounded number of query answers taking values from the set of reals. This is joint work with Rohit Chadha and Prasad Sistla. Bio: Mahesh Viswanathan is a faculty member at the University of Illinois at Urbana-Champaign. His research interests are in the core areas of logic, automata theory, and algorithm design, with applications to the algorithmic verification of systems. Most recently, his research has been focussed on the dynamic analysis of multi-threaded programs, model checking of cyberphysical systems and stochastic systems, and formal analysis of stochastic security protocols and differential privacy.