Verified software: from theory to practice

Workshop theme

Formal methods for the specification and verification of software-intensive systems bridge the gap between theory and applications. Verification techniques have to be tuned to application areas such as concurrency, cyber-physical systems, distributed systems, machine learning, computer security, networks, and programming languages. The INI Virtual Workshop is a precursor event to the program on Verified Software. It will involve an intensive exchange of ideas between researchers facing the challenges of cutting-edge applications and theoreticians armed with the conceptual tools to potentially address these challenges.

Given the current restrictions on movement, due to the ongoing pandemic, the INI intends to run this workshop virtually across 5 days. All talks and discussion sessions will be available virtually.

Timetable

Monday 10th May 2021
15:30 to 15:50	Chair: Azadeh Farzan Social	Room 1
15:50 to 16:00	Christie Marr Isaac Newton Institute Chair: Azadeh Farzan Welcome Talk	Room 1
16:00 to 16:30	Tony Hoare Isaac Newton Institute Chair: Azadeh Farzan VSI: A Personal History of its Early Origins	Room 1
16:30 to 17:00	Maurice Herlihy Brown University; Brown University Chair: Azadeh Farzan Verifying Smart Contracts	Room 1
17:00 to 17:30	Break	Room 1
17:30 to 18:00	Anca Muscholl University of Bordeaux Chair: Azadeh Farzan Learning Sound Negotiations	Room 1
18:00 to 18:30	Ahmed Bouajjani Université Paris 7 - Denis-Diderot Chair: Azadeh Farzan Verification of Concurrent Programs under Persistent Weak Memory Models	Room 1
18:30 to 19:00	Rupak Majumdar Max Planck Institute for Software Systems Chair: Azadeh Farzan Random Testing and Formal Methods	Room 1

Tuesday 11th May 2021
15:30 to 16:00	Ilya Sergey Yale-NUS College; National University of Singapore Chair: Philippa Gardner Practical Smart Contract Sharding with Ownership and Commutativity Analysis	Room 1
16:00 to 16:30	Lars Birkedal Aarhus Universitet Chair: Philippa Gardner Program Verification on a Capability Machine in the Presence of Untrusted Code	Room 1
16:30 to 17:00	Amal Ahmed Northeastern University Chair: Philippa Gardner Verifying Soundness of Foreign-Function Interfaces	Room 1
17:00 to 17:30	Break	Room 1
17:30 to 18:00	Viktor Vafeiadis Max Planck Institute for Software Systems Chair: Philippa Gardner Making Stateless Model Checking Stateless Again	Room 1
18:00 to 18:30	Aarti Gupta Princeton University Chair: Philippa Gardner Abstract Interpretation of Distributed Network Control Planes	Room 1
18:30 to 19:00	Alexandra Silva University College London Chair: Philippa Gardner Prognosis: Black-Box Analysis of Network Protocol Implementations	Room 1

Wednesday 12th May 2021
15:30 to 16:00	Véronique Cortier Lorraine Research Laboratory in Computer Science and its Applications Chair: Peter O'Hearn Formal Verification of Security Protocols - The Example of Electronic Voting	Room 1
16:00 to 16:30	Karthikeyan Bhargavan INRIA Chair: Peter O'Hearn Putting Verified Crypto into Your Web Browser	Room 1
16:30 to 17:00	Justin Hsu University of Wisconsin-Madison Chair: Peter O'Hearn Data-Driven Invariant Learning for Probabilistic Programs	Room 1
17:00 to 17:30	Break	Room 1
17:30 to 18:00	Zachary Kincaid Princeton University Chair: Natarajan Shankar Robust Program Analysis	Room 1
18:00 to 18:30	Jean-Francois Raskin Université Libre de Bruxelles Chair: Natarajan Shankar Monte Carlo Tree Search Guided by Symbolic Advice for MDPs	Room 1
18:30 to 19:00	Javier Esparza Technische Universität München Chair: Natarajan Shankar Verifying Almost-Sure Termination of Replicated Systems	Room 1

Thursday 13th May 2021
15:30 to 16:00	Hongseok Yang Korea Advanced Institute of Science and Technology (KAIST) Chair: Peter Sewell Towards Verified Stochastic Variational Inference for Probabilistic Programs	Room 1
16:00 to 16:30	Marta Zofia Kwiatkowska University of Oxford Chair: Peter Sewell Probabilistic Model Checking for the Data-Rich World	Room 1
16:30 to 17:00	Martin Vechev ETH Zürich Chair: Peter Sewell Certified Deep Learning	Room 1
17:00 to 17:30	Break	Room 1
17:30 to 18:00	Adam Chlipala Massachusetts Institute of Technology Chair: Natarajan Shankar Fiat Cryptography: A Code-Generation Approach to Correct-by-Construction Cryptography	Room 1
18:00 to 18:30	Jade Alglave University College London; ARM Chair: Natarajan Shankar Arm Memory Model	Room 1
18:30 to 19:00	Annabelle McIver Macquarie University Chair: Natarajan Shankar How to change a Government's mind	Room 1

Friday 14th May 2021
15:30 to 16:00	Thomas Henzinger IST Austria Chair: Moshe Vardi Quantitative and Approximate Monitoring	Room 1
16:00 to 16:30	Sanjit Seshia University of California, Berkeley Chair: Moshe Vardi Algorithmic Improvisation for Verified Autonomy	Room 1
16:30 to 17:00	Pavithra Prabhakar Kansas State University Chair: Moshe Vardi Abstractions for Scalable Verification of AI-Controlled Cyber-Physical Systems (CPS)	Room 1
17:00 to 17:30	Break	Room 1
17:30 to 18:00	Madhusudan Parthasarathy University of Illinois at Urbana-Champaign Chair: Moshe Vardi Automating Logic Reasoning for Building Verified Software	Room 1
18:00 to 18:30	Rajeev Alur University of Pennsylvania Chair: Moshe Vardi Formal Verification for Safe Autonomy	Room 1

Organisers

Leonardo de Moura Microsoft (UK)
Azadeh Farzan University of Toronto
Philippa Gardner Imperial College London
Kim Larsen Aalborg Universitet
Xavier Leroy Collège de France; INRIA
Ken McMillan Microsoft (USA)
Peter O'Hearn University College London
Peter Sewell University of Cambridge
Natarajan Shankar
Moshe Vardi Rice University

Speakers

Amal Ahmed Northeastern University
Ahmed Bouajjani Université Paris 7 - Denis-Diderot
Adam Chlipala Massachusetts Institute of Technology
Annabelle McIver Macquarie University
Sanjit Seshia University of California, Berkeley
Alexandra Silva University College London
Viktor Vafeiadis Max Planck Institute for Software Systems
Jade Alglave University College London; ARM
Rajeev Alur University of Pennsylvania
Karthikeyan Bhargavan INRIA
Lars Birkedal Aarhus Universitet
Véronique Cortier Lorraine Research Laboratory in Computer Science and its Applications
Javier Esparza Technische Universität München
Aarti Gupta Princeton University
Thomas Henzinger IST Austria
Maurice Herlihy Brown University; Brown University
Tony Hoare
Justin Hsu University of Wisconsin-Madison
Zachary Kincaid Princeton University
Marta Zofia Kwiatkowska University of Oxford
Rupak Majumdar Max Planck Institute for Software Systems
Anca Muscholl University of Bordeaux
Madhusudan Parthasarathy University of Illinois at Urbana-Champaign
Pavithra Prabhakar Kansas State University
Jean-Francois Raskin Université Libre de Bruxelles
Ilya Sergey Yale-NUS College; National University of Singapore
Martin Vechev ETH Zürich
Hongseok Yang Korea Advanced Institute of Science and Technology (KAIST)

Show All

Participants

Amal Ahmed Northeastern University
Ahmed Bouajjani Université Paris 7 - Denis-Diderot
Adam Chlipala Massachusetts Institute of Technology
Anil Madhavapeddy Cambridge Computer Laboratory
Annabelle McIver Macquarie University
Benjamin Pierce University of Pennsylvania
Sanjit Seshia University of California, Berkeley
Alexandra Silva University College London
Viktor Vafeiadis Max Planck Institute for Software Systems
Mohammad Abdulaziz Australian National University
Benedikt Ahrens INRIA Rennes - Bretagne Atlantique
Jade Alglave University College London; ARM
Rajeev Alur University of Pennsylvania
Amer Tahat Amertahat Virginia Polytechnic Institute and State University
Jie An Max Planck Institute for Software Systems
Roberto Bagnara Università degli Studi di Parma
Clark Barrett Stanford University
Andreas Bender Università degli Studi di Pavia
Lennart Beringer Princeton University
Karthikeyan Bhargavan INRIA
Lars Birkedal Aarhus Universitet
Roberto Blanco None / Other
Alexandre Bouayad University of Cambridge
Andrea Bracciali University of Stirling
Martin Brain City, University of London; University of Oxford
Franck Cassez None / Other; Macquarie University
Supratik Chakraborthy Indian Institute of Technology
Aurek Chattopadhyay National Institute of Technology Rourkela
Mingshuai Chen RWTH Aachen University
Jiawei Chen University of Michigan
Egon Cholakian Harvard University
Daniela Cialfi Simons Foundation
Michael Conard Michigan Technological University
Véronique Cortier Lorraine Research Laboratory in Computer Science and its Applications
Denis Cousineau Mitsubishi Electric
Florin Craciun Babes,-Bolyai University
Emanuele D'osualdo Max Planck Institute for Software Systems
Pallab Dasgupta Indian Institute of Technology
Leonardo de Moura Microsoft (UK)
Paulo de Vilhena INRIA Paris - Rocquencourt
Delphine Demange Université de Rennes 1
Dominique Devriese Vrije Universiteit Brussel
Praveen Kumar Dhankar Rashtrasant Tukadoji Maharaj Nagpur University; Rashtrasant Tukadoji Maharaj Nagpur University
Jonathan Dixon University of Cambridge
Damien Doligez INRIA
Ke Du University of Illinois at Chicago
Stefania Dumbrava None / Other
Madalina Erascu Universitatea de Vest din Timisoara
Levent Erkok None / Other
Javier Esparza Technische Universität München
Azadeh Farzan University of Toronto
Ramon Fernandez Mir University of Edinburgh
Cameron Freer Massachusetts Institute of Technology
Marianne Freiberger University of Cambridge
Ming Fu None / Other
Philippa Gardner Imperial College London
Aarti Gupta Princeton University
Marton Hajdu Vienna University of Technology
William Hallahan Yale University
Ian Hayes University of Queensland
Siyuan He Purdue University
Thomas Henzinger IST Austria
Maurice Herlihy Brown University; Brown University
Tony Hoare
Douglas Howe None / Other
Justin Hsu University of Wisconsin-Madison
Paul Jackson University of Edinburgh
Cliff Jones Newcastle University
Chandan Karfa Indian Institute of Technology
Mansur Khazeev Innopolis University
Daniel Kienitz Heriot-Watt University
Zachary Kincaid Princeton University
Michal Konecny Aston University
Sivasankara Rao Kotha Anna University
Kamil Kulesza Polish Academy of Sciences
Marta Zofia Kwiatkowska University of Oxford
Ori Lahav Tel Aviv University
Kim Larsen Aalborg Universitet
Xavier Leroy Collège de France; INRIA
Marco Lewis Newcastle University
Yi Li Peking University
Xiaokun Luan Peking University
Ziyan Luo McGill University
Christopher Lynch Clarkson University
Andreas Lööw Chalmers University of Technology
Jean-Marie Madiot Madiot INRIA
Rupak Majumdar Max Planck Institute for Software Systems
Petar Maksimovic Imperial College London
Ken McMillan Microsoft (USA)
Ricardo Medel None / Other
Jayadev Misra University of Texas at Austin
Ugo Montanari Università di Pisa
Carlo Montangero Università di Pisa
Marcel Moosbrugger Vienna University of Technology
Anca Muscholl University of Bordeaux
Cesar Muñoz NASA Langley Research Center
David Naumann Stevens Institute of Technology
Duc Than Nguyen University of Illinois at Chicago
Peter O'Hearn University College London
Duckki Oe None / Other
Prakash Panangaden McGill University
Jun Pang Université du Luxembourg
Thomas Pani Technische Universität Wien
Madhusudan Parthasarathy University of Illinois at Urbana-Champaign
Andrei Paskevich Université Paris Saclay
Jorge Perez University of Groningen
Jean Pichon-Pharabod University of Cambridge
Ruzica Piskac Yale University
Andreas Podelski Albert-Ludwigs-Universität Freiburg
Pavithra Prabhakar Kansas State University
Maben Rabi None / Other
Sophie Rain Vienna University of Technology
Jason Ralph University of Liverpool
Subramanian Ramamoorthy University of Edinburgh
Raghavendra Ramesh ConsenSys
Steven Ramsay University of Bristol
Francesco Ranzato Università degli Studi di Padova
Xiaojia Rao Imperial College London
Junaid Rasheed Aston University
Jean-Francois Raskin Université Libre de Bruxelles
Wrenna Robson Royal Holloway, University of London
Didier Rémy INRIA
Karem Sakallah University of Michigan
Asieh Salehi Fathabadi University of Southampton
Ilya Sergey Yale-NUS College; National University of Singapore
Peter Sewell University of Cambridge
Ramy Shahin University of Toronto
Natarajan Shankar
Arpit Sharma Indian Institute of Science Education and Research (IISER)
Nikolay Shilov Innopolis University
Xujie Si McGill University
William Simmons Carnegie Mellon University
Manish Singh Victoria University of Wellington
Abhishek Singh None / Other; Tata Institute of Fundamental Research
Robert Soeldner University of York
Matthieu Sozeau INRIA Rennes - Bretagne Atlantique; Université de Nantes
Andrzej Tarlecki Uniwersytet Warszawski
Rachel Thomas University of Cambridge
Palina Tolmach Nanyang Technological University
Christian Urban King's College London
Moshe Vardi Rice University
Martin Vechev ETH Zürich
Philip Wadler University of Edinburgh
Jingyi Wang Zhejiang University
Ziyan Wang None / Other
Conrad Watt University of Cambridge
Tjark Weber Uppsala Universitet
Thomas Wies New York University
Herbert Wiklicky Imperial College London
Xiuheng Wu Nanyang Technological University
Yushuo Xiao Peking University
Ningning Xie University of Hong Kong
Boris Yakobowski None / Other
Hongseok Yang Korea Advanced Institute of Science and Technology (KAIST)
Nobuko Yoshida Imperial College London
Chenyang Zhu University of Southampton; University of Pennsylvania
Paolo Zuliani Newcastle University