How Do We Read Formal Claims? Eye-Tracking and the Cognition of Proofs about Algorithms
Formal methods are used successfully in high-assurance software, but they require rigorous mathematical and logical training that practitioners often lack. As such, integrating formal methods into software has been associated with numerous challenges. While educators have placed emphasis on formalisms in undergraduate theory courses, such courses often struggle with poor student outcomes and satisfaction. In this paper, we present a controlled eye-tracking human study (n=34) investigating the problem-solving strategies employed by students with different levels of incoming preparation, and how educators can better prepare low-outcome students for the rigorous logical reasoning that is a core part of formal methods in software engineering. We find that incoming preparation is not a good predictor of student outcomes for formalism comprehension tasks, and that student self-reports are not accurate at identifying factors associated with high outcomes for such tasks. Instead and importantly, we find that differences in outcomes can be attributed to performance for proofs by induction and recursive algorithms, and that better-performing students exhibit significantly more attention switching behaviors, a result that has several implications for pedagogy in terms of the design of teaching materials. Our results suggest the need for a substantial pedagogical intervention in core theory courses to better align student outcomes with the objectives of mastery and retaining the material, and thus bettering preparing them for high-assurance software engineering.
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:00 15mTalk | 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 15mTalk | Which of My Assumptions are Unnecessary for Realizability and Why Should I Care? Technical Track Pre-print | ||
11:30 15mTalk | 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 15mTalk | 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 7mTalk | 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 7mTalk | CoVeriTeam Service: Verification as a Service DEMO - Demonstrations | ||
12:15 7mTalk | 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 7mTalk | 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 |