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
09:00 to 17:00	VSOW03 Verified software: from theory to practice	Room 1
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 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 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 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

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

Speakers

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

Show All

Participants

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