Verified software: tools and experiments

Workshop theme

The Tools and Experiments workshop is aimed at defining an integrated tool resources for automated formal methods with standardized interfaces and interchange and data/evidence formats that allow services and arguments to be composed and test cases and counterexamples to be shared across different formal models. The goal of the INI Virtual Workshop is to lay the foundation for powerful automated tools and integrated tool suites that can be deployed in a range of large-scale experiments and case studies.

The workshop will include a special event marking the 60th anniversary of Tony Hoare's invention of Quicksort.

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.

Deadline for applications: 20th May 2021

Applications for this workshop are now closed

Timetable

Monday 7th June 2021
15:30 to 15:55	Natarajan Shankar SRI International Chair: Cliff Jones Welcome	Room 1
15:55 to 16:00	Christie Marr Isaac Newton Institute Welcome Talk	Room 1
16:00 to 16:30	Douglas McIlroy Dartmouth College Chair: Cliff Jones Folklore of Computational Complexity	Room 1
16:30 to 17:00	Robert Sedgewick Princeton University Chair: Cliff Jones What Do We Know About Quicksort?	Room 1
17:30 to 18:00	Sebastian Wild University of Liverpool Chair: Cliff Jones Quicksorts of the 21st century	Room 1
18:00 to 18:30	Tony Hoare Isaac Newton Institute Chair: Cliff Jones Tony Hoare Answers Questions	Room 1

Tuesday 8th June 2021
15:30 to 16:00	Naijun Zhan Chinese Academy of Sciences Chair: Kim Guldstrand Larsen Extending Hoare Logic to Hybrid Systems	Room 1
16:00 to 16:30	Andre Platzer Carnegie Mellon University Chair: Kim Guldstrand Larsen The Logical Path to Autonomous Cyber-Physical Systems	Room 1
16:30 to 17:00	Armin Biere Johannes Kepler Universität Chair: Kim Guldstrand Larsen Fueling the SAT Revolution	Room 1
17:30 to 18:00	Bernd Finkbeiner Universität des Saarlandes Chair: Kim Guldstrand Larsen Tools for the Automated Verification of Hyperproperties	Room 1
18:00 to 18:30	Cesare Tinelli University of Iowa Chair: Kim Guldstrand Larsen The Persisting Challenge of Reasoning About Quantified Formulas Modulo Theories	Room 1
18:30 to 19:00	Warren Hunt University of Texas at Austin Chair: Kim Guldstrand Larsen The Industrial Use of ACL2 for Hardware Verification	Room 1

Wednesday 9th June 2021
15:30 to 16:00	Mooly Sagiv Tel Aviv University Chair: Xavier Leroy Formal Reasoning about Decentralized Financial Applications	Room 1
16:00 to 16:30	Supratik Chakraborty Indian Institute of Technology Chair: Xavier Leroy Full-Program Induction for Verifying Array Manipulating Programs	Room 1
16:30 to 17:00	Peter Müller ETH Zürich Chair: Xavier Leroy Leveraging Rust Types for Modular Specification and Verification	Room 1
17:30 to 18:00	Matthias Heizmann Albert-Ludwigs-Universität Freiburg Chair: Natarajan Shankar Traces, Interpolants, and Automata : Ultimate Automizer's Approach to Software Verification	Room 1
18:00 to 18:30	Roderick Bloem Graz University of Technology Chair: Natarajan Shankar Side Channel Secure Software	Room 1
18:30 to 19:00	Marieke Huisman Universiteit Twente Chair: Natarajan Shankar VerCors: A Program Verifier for Concurrent Software	Room 1

Thursday 10th June 2021
15:30 to 16:00	Orna Grumberg Technion - Israel Institute of Technology Chair: Ken McMillan Remembering Ed Clarke	Room 1
16:00 to 16:30	Kedar Namjoshi Nokia Bell Labs Chair: Ken McMillan Remembering Bob Kurshan	Room 1
16:30 to 17:00	Aarti Gupta Princeton University ; David Dill None / Other; Stanford University ; Randal Bryant Carnegie Mellon University ; Somesh Jha University of Wisconsin-Madison Chair: Ken McMillan Remembering Ed Clarke and Bob Kurshan	Room 1
17:30 to 18:00	Emina Torlak University of Washington Chair: Ken McMillan Solver-aided verification for systems software	Room 1
18:00 to 18:30	Nate Foster Cornell University; Intel Chair: Ken McMillan Toward Verified Data Planes	Room 1
18:30 to 19:00	Daniel Schwartz-Narbonne Amazon Web Services Chair: Ken McMillan RMC: A Bit-Precise Model-Checker for Rust	Room 1

Friday 11th June 2021
15:30 to 16:00	Lenore Zuck University of Illinois at Chicago Chair: Xavier Leroy A Teaspoon of Formal Methods	Room 1
16:00 to 16:30	Benjamin Pierce University of Pennsylvania Chair: Xavier Leroy Property-Based Testing for Networked Servers: The DeepWeb Experience	Room 1
16:30 to 17:00	Ranjit Jhala University of California, San Diego Chair: Xavier Leroy Modular Specification and Decidable Verification using Abstract Refinement Types	Room 1
17:30 to 18:00	Nadia Polikarpova University of California, San Diego Chair: Natarajan Shankar Synthesis of Safe Pointer-Manipulating Programs	Room 1
18:00 to 18:30	Armando Solar-Lezama Massachusetts Institute of Technology Chair: Natarajan Shankar The Creation and Evolution of the Sketch Synthesis System	Room 1
18:30 to 19:00	Ruzica Piskac Yale University Chair: Natarajan Shankar Counterexample Guided Inference of Modular Specifications	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

Orna Grumberg Technion - Israel Institute of Technology
Benjamin Pierce University of Pennsylvania
Armin Biere Johannes Kepler Universität
Roderick Bloem Graz University of Technology
Randal Bryant Carnegie Mellon University
Supratik Chakraborty Indian Institute of Technology
David Dill None / Other; Stanford University
Bernd Finkbeiner Universität des Saarlandes
Nate Foster Cornell University; Intel
Aarti Gupta Princeton University
Matthias Heizmann Albert-Ludwigs-Universität Freiburg
Tony Hoare Isaac Newton Institute
Marieke Huisman Universiteit Twente
Warren Hunt University of Texas at Austin
Somesh Jha University of Wisconsin-Madison
Ranjit Jhala University of California, San Diego
Christie Marr Isaac Newton Institute
Douglas McIlroy Dartmouth College
Peter Müller ETH Zürich
Kedar Namjoshi Nokia Bell Labs
Ruzica Piskac Yale University
Andre Platzer Carnegie Mellon University
Nadia Polikarpova University of California, San Diego
Mooly Sagiv Tel Aviv University
Daniel Schwartz-Narbonne Amazon Web Services
Robert Sedgewick Princeton University
Natarajan Shankar SRI International
Armando Solar-Lezama Massachusetts Institute of Technology
Cesare Tinelli University of Iowa
Emina Torlak University of Washington
Sebastian Wild University of Liverpool
Naijun Zhan Chinese Academy of Sciences
Lenore Zuck University of Illinois at Chicago

Show All