This program is tentative and subject to change.

Wed 17 Jul 2024 11:27 - 11:36 at Baobá 2 - Formal Verification

This paper presents \emph{verification-guided development} (VGD), a software development process that we used to develop Cedar, a new policy language for expressive, fast, safe, and analyzable authorization. Developing a system with VGD involves two activities: (1) writing a readable, executable model of the system and proving mechanically-verified properties about it; and (2) writing production code for the system, using extensive \emph{differential random testing} (DRT) to check that the production code’s behavior matches that of the model, and \emph{property-based testing} (PBT) to check properties of unmodeled components of the production code. Using VGD for Cedar has been beneficial: we are able to build fast, idiomatic production code and find and fix bugs during the development phase: when carrying out proofs we found and fixed four soundness bugs in Cedar’s policy validator, and when carrying out DRT and PBT we found and fixed 21 bugs in the Cedar parser, evaluator, authorizer, and validator.

This program is tentative and subject to change.

Wed 17 Jul

Displayed time zone: Brasilia, Distrito Federal, Brazil change

11:00 - 12:30
11:00
18m
Talk
A Transferability Study of Interpolation-Based Hardware Model Checking to Software Verification
Research Papers
Dirk Beyer LMU Munich, Po-Chun Chien LMU Munich, Marek Jankola LMU Munich, Nian-Ze Lee LMU Munich
11:18
9m
Talk
CoqPyt: Proof Navigation in Python in the Era of LLMs
Demonstrations
Pedro Carrott Imperial College London, Nuno Saavedra INESC-ID and IST, University of Lisbon, Kyle Thompson University of California, San Diego, Sorin Lerner University of California at San Diego, João F. Ferreira INESC-ID and IST, University of Lisbon, Emily First University of California, San Diego
DOI Pre-print
11:27
9m
Talk
How We Built Cedar: A Verification-Guided Approach
Industry Papers
Craig Disselkoen Amazon Web Services, Aaron Eline Amazon, Shaobo He Amazon Web Services, Kyle Headley Unaffiliated, MIchael Hicks Amazon, Kesha Hietala Amazon Web Services, John Kastner Amazon Web Services, Anwar Mamat University of Maryland, Matt McCutchen , Neha Rungta Amazon Web Services, Bhakti Shah University of Chicago, Emina Torlak Amazon Web Services, USA, Andrew Wells Amazon Web Services
11:36
18m
Talk
Mission Specification Patterns for Mobile Robots: Providing Support for Quantitative Properties
Journal First
Claudio Menghi University of Bergamo; McMaster University, Christos Tsigkanos University of Bern, Switzerland, Mehrnoosh Askarpour McMaster University, Patrizio Pelliccione Gran Sasso Science Institute, L'Aquila, Italy, Gricel Vázquez University of York, UK, Radu Calinescu University of York, UK, Sergio García Volvo Cars Corporation, Sweden
11:54
18m
Talk
Rigorous Assessment of Model Inference Accuracy using Language Cardinality
Journal First
Donato Clun Imperial College London, Donghwan Shin University of Sheffield, Antonio Filieri AWS and Imperial College London, Domenico Bianculli University of Luxembourg
12:12
18m
Talk
Simulation-based Testing of Simulink Models with Test Sequence and Test Assessment Blocks
Journal First
Federico Formica McMaster University, Tony Fan McMaster University, Akshay Rajhans Mathworks, Vera Pantelic McMaster University, Mark Lawford McMaster University, Claudio Menghi University of Bergamo; McMaster University