2022/03/22 by Liam O'Connor, Liam O’Connor, O'Connor, Liam +2 · 1 voice
Computer Science · #Advanced Malware Detection Techniques #FOS: Computer and information sciences #Formal Methods in Verification #Programming Languages (cs.PL) #Software Engineering (cs.SE) #Software Testing and Debugging Techniques #cs.PL #cs.SE
paper · pdf · doi:10.48550/arxiv.2203.11532
13 pages, this is a technical report of a paper to appear at Programming Languages Design and Implementation (PLDI 2022)
arxiv created 2022/03/22 · openalex publication_date 2022/03/22 · arxiv published 2022/03/22 · arxiv updated 2022/03/23 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/01
We present Quickstrom, a property-based testing system for acceptance testing of interactive applications. Using Quickstrom, programmers can specify the behaviour of web applications as properties in our testing-oriented dialect of Linear Temporal Logic (LTL) called QuickLTL, and then automatically test their application against the given specification with hundreds of automatically generated interactions. QuickLTL extends existing finite variants of LTL for the testing use-case, determining likely outcomes from partial traces whose minimum length is itself determined by the LTL formula. This temporal logic is embedded in our specification language, Specstrom, which is designed to be approachable to web programmers, expressive for writing specifications, and easy to analyse. Because Quickstrom tests only user-facing behaviour, it is agnostic to the implementation language of the system under test. We therefore formally specify and test many implementations of the popular TodoMVC benchmark, used for evaluation and comparison across various web frontend frameworks and languages. Our tests uncovered bugs in almost half of the available implementations.