Write a Blog >>
ICSE 2023
Sun 14 - Sat 20 May 2023 Melbourne, Australia
Wed 17 May 2023 11:15 - 11:30 at Meeting Room 104 - Formal verification Chair(s): Bonita Sharif

Specifications for reactive systems synthesis consist of assumptions and guarantees. However, some specifications may include unnecessary assumptions, i.e., assumptions that are not necessary for realizability. While the controllers that are synthesized from such specifications are correct, they are also inflexible and fragile; their executions will satisfy the specification’s guarantees in only very specific environments.

In this work we show how to detect unnecessary assumptions, and to transform any realizable specification into a corresponding realizable core specification, one that includes the same guarantees but no unnecessary assumptions. We do this by computing an assumptions core, a locally minimal subset of assumptions that suffices for realizability. Controllers that are synthesized from a core specification are not only correct but, importantly, more general; their executions will satisfy the specification’s guarantees in more environments.

We implemented our ideas in the Spectra synthesis environment, and evaluated their impact over different benchmarks from the literature. The evaluation provides evidence for the motivation and significance of our work, by showing (1) that unnecessary assumptions are highly prevalent, (2) that in almost all cases the fully-automated removal of unnecessary assumptions pays off in total synthesis time, and (3) that core specifications induce more general controllers whose reachable state space is larger but whose representation more memory efficient.

Wed 17 May

Displayed time zone: Hobart change

11:00 - 12:30
11:00
15m
Talk
How Do We Read Formal Claims? Eye-Tracking and the Cognition of Proofs about Algorithms
Technical Track
Hammad Ahmad University of Michigan, Zachary Karas University of Michigan, Kimberly Diaz University of Michigan, Amir Kamil University of Michigan, Jean-Baptiste Jeannin University of Michigan at Ann Arbor, Westley Weimer University of Michigan
11:15
15m
Talk
Which of My Assumptions are Unnecessary for Realizability and Why Should I Care?
Technical Track
Rafi Shalom Tel Aviv University, Israel, Shahar Maoz Tel Aviv University
Pre-print
11:30
15m
Talk
Understanding Inconsistency in Azure Cosmos DB with TLA+
SEIP - Software Engineering in Practice
Alistair Finn Hackett University of British Columbia, Joshua Rowe Microsoft, Markus Alexander Kuppe Microsoft Research
11:45
15m
Talk
Rely/Guarantee Reasoning for Multicopy Atomic Weak Memory Models
Showcase
Nicholas Coughlin Defence Science and Technology Group, Australia, Kirsten Winter Defence Science and Technology Group, Australia, Graeme Smith The University of Queensland
12:00
7m
Talk
HOME: Heard-Of based Formal Modeling and Verification Environment for Consensus Protocols
DEMO - Demonstrations
Shumao Zhai Beihang University, Xiaozhou Li University of Oulu, Ning Ge School of Software, Beihang University
12:07
7m
Talk
CoVeriTeam Service: Verification as a Service
DEMO - Demonstrations
Dirk Beyer LMU Munich, Sudeep Kanav LMU Munich, Henrik Wachowitz LMU Munich
12:15
7m
Talk
Proofster: Automated Formal Verification
DEMO - Demonstrations
Arpan Agrawal University of Illinois Urbana-Champaign, Emily First University of Massachusetts Amherst, Zhanna Kaufman University of Massachusetts, Tom Reichel University of Illinois Urbana-Champaign, Shizhuo Zhang University of Illinois Urbana-Champaign, Timothy Zhou University of Illinois Urbana-Champaign, Alex Sanchez-Stern University of Massachusetts at Amherst, Talia Ringer University of Illinois at Urbana-Champaign, Yuriy Brun University of Massachusetts
Media Attached
12:22
7m
Talk
Anti-Patterns (Smells) in Temporal Specifications
NIER - New Ideas and Emerging Results
Dor Ma'ayan Tel Aviv University, Shahar Maoz Tel Aviv University, Jan Oliver Ringert Bauhaus-University Weimar
Pre-print