Anti-Patterns (Smells) in Temporal Specifications
Temporal specifications are essential inputs for verification and synthesis. Despite their importance, temporal specifications are challenging to write, which might limit their use by software engineers. To this day, almost no quality attributes of temporal specifications have been defined and investigated. Our work takes a first step toward exploring and improving the quality of temporal specifications by proposing a preliminary catalog of anti-patterns (a.k.a. smells). We base the catalog on our experience in developing and teaching temporal specifications for verification and synthesis. In addition, we examined publicly available specification repositories and relevant literature. Finally, we outline our future plans for a better understanding of what constitutes high-quality temporal specifications and the development of tools that will help engineers write them.
Wed 17 MayDisplayed time zone: Hobart change
| 11:00 - 12:30 | Formal verificationSEIP - Software Engineering in Practice / DEMO - Demonstrations / Technical Track / NIER - New Ideas and Emerging Results / Showcase at Meeting Room 104 Chair(s): Bonita Sharif University of Nebraska-Lincoln, USA | ||
| 11:0015m 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:1515m Talk | Which of My Assumptions are Unnecessary for Realizability and Why Should I Care? Technical TrackPre-print | ||
| 11:3015m Talk | Understanding Inconsistency in Azure Cosmos DB with TLA+ SEIP - Software Engineering in Practice Finn Hackett University of British Columbia, Joshua Rowe Microsoft, Markus Alexander Kuppe Microsoft Research | ||
| 11:4515m 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:007m 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:077m Talk | CoVeriTeam Service: Verification as a Service DEMO - Demonstrations | ||
| 12:157m 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 MassachusettsMedia Attached | ||
| 12:227m 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 WeimarPre-print | ||


