Wed 21 Jun 2023 09:40 - 10:00 at Royal - PLDI: Testing & Verification Chair(s): Yao Li

The conformance testing of programming language implementations is crucial to support correct and consistent execution environments. Because manually maintaining conformance tests for real-world programming languages is cumbersome and labor-intensive, researchers have presented various ways to make conformance tests effective and efficient. One such approach is to use graph coverage, one of the most widely-used coverage criteria, to generate tests that reach different parts of a mechanized language specification. Since mechanized specifications use functions or inductive definitions to describe the semantics of language features, traditional graph coverage criteria for software work as they are. However, they may not produce high-quality conformance tests because language implementations often have specialized execution paths for different features, even when their semantics descriptions use the same functions. Traditional graph coverage may not distinguish test requirements of such language features, which degrades the quality of conformance testing. Similarly, it may not distinguish test requirements of different parts of the same language feature when their semantics descriptions use the same functions.

We present feature-sensitive (FS) coverage as a novel coverage criterion to generate high-quality conformance tests for language implementations. It is a general extension of graph coverage, refining conventional test requirements using the innermost enclosing language features. We also introduce feature-call-path-sensitive (FCPS) coverage, a variant of FS coverage, and extend both coverage criteria using the 𝑘-limiting approach. To evaluate the effectiveness of the new coverage criteria for language implementations, we apply them to a mechanized specification of JavaScript. We extend JEST, the state-of-the-art JavaScript conformance test synthesizer using coverage-guided mutational fuzzing, with various FS and FCPS coverage criteria. For the latest JavaScript language specification (ES13, 2022), our tool automatically synthesizes 237,981 conformance tests in 50 hours with five coverage criteria. We evaluated the conformance of eight mainstream JavaScript implementations (four engines and four transpilers) with the synthesized conformance tests and discovered bugs in all of them. The tool detected 143 distinct conformance bugs (42 in engines and 101 in transpilers), 85 of which were confirmed by the developers and 83 of which were newly discovered bugs.

Wed 21 Jun

Displayed time zone: Eastern Time (US & Canada) change

09:00 - 11:00
PLDI: Testing & VerificationPLDI Research Papers at Royal
Chair(s): Yao Li Portland State University

#pldi-wed-0900-testing-royal Discord icon small YouTube icon small

09:00
20m
Talk
Mostly Automated Proof Repair for Verified LibrariesDistinguished Paper
PLDI Research Papers
Kiran Gopinathan National University of Singapore, Mayank Keoliya National University of Singapore, Ilya Sergey National University of Singapore
DOI Pre-print
09:20
20m
Talk
Proving and Disproving Equivalence of Functional Programming Assignments
PLDI Research Papers
Dragana Milovancevic EPFL, Viktor Kunčak EPFL, Switzerland
DOI Pre-print
09:40
20m
Talk
Feature-Sensitive Coverage for Conformance Testing of Programming Language Implementations
PLDI Research Papers
Jihyeok Park Korea University, Dongjun Youn KAIST, Kanguk Lee KAIST, Sukyoung Ryu KAIST
DOI Pre-print
10:00
20m
Talk
Psym: Efficient Symbolic Exploration of Distributed Systems
PLDI Research Papers
Lauren Pick University of Wisconsin-Madison and University of California, Berkeley, Ankush Desai Amazon Web Services, Aarti Gupta Princeton University
DOI
10:20
20m
Talk
Modular Control Plane Verification via Temporal Invariants
PLDI Research Papers
Tim Alberdingk Thijm Princeton University, Ryan Beckett Microsoft Research, USA, Aarti Gupta Princeton University, David Walker Princeton University
DOI
10:40
20m
Talk
Fair Operational Semantics
PLDI Research Papers
Dongjae Lee Seoul National University, Minki Cho Seoul National University, Jinwoo Kim Seoul National University, Soonwon Moon Inha University, Youngju Song MPI-SWS, Chung-Kil Hur Seoul National University
DOI