プログラム

座長: 沢田 篤史 (南山大学)

座長: 林 晋平 (東京工業大学)

座長: 丸山 宏 (Preferred Networks/東大/花王)

トップカンファレンス・トップ論文誌特別講演（FOSE）8/31 【16:50～18:05】

• 劉 少英（広島大学）
  講演タイトル: 「Automatic Test Case and Test Oracle Generation Based on Functional Scenarios in Formal Specifications for Conformance Testing」
  掲載誌: IEEE TSE
  講演概要: Testing a program to confirm whether it consistently implements its requirements specification is a necessary but time-consuming activity in software development. Automatic testing based on specifications can significantly alleviate the workload and cost, but faces a challenge of how to ensure that both the user’s concerns in the specification and possible execution paths in the program are all covered. In this paper, we describe a new method, called “Vibration-Method” or simply “V-Method”, for automatic generation of test cases and test oracle from model-based formal specifications, aiming to address this challenge. The proposed method is suitable for testing information systems in which rich data types are used. Supporting the principle of “divide and conquer”, the method provides a specific technique for generating test cases based on functional scenarios defined in the specification, test case generation criteria, automatic test case generation algorithms, and a well-defined mechanism for deriving test oracle. We elaborate on the method by discussing how initial test cases can be automatically generated, how additional necessary test cases are produced using the “vibration” technique, and how a test oracle can be automatically derived for a group of test cases. We also describe a controlled experiment to evaluate the effectiveness of the method and discuss the important issues in relation to the performance and applicability of the method.

• 肥後 芳樹（大阪大学）
  講演タイトル: 「NIL: large-scale detection of large-variance clones」
  発表会議名: ESEC/FSE 2021
  講演概要: A code clone (in short, clone) is a code fragment that is identical or similar to other code fragments in source code. Clones generated by a large number of changes to copy-and-pasted code fragments are called large-variance (modifications are scattered) or large-gap (modifications are in one place) clones. It is difficult for general clone detection techniques to detect such clones and thus specialized techniques are necessary. In addition, with the rapid growth of software development, scalable clone detectors that can detect clones in large codebases are required. However, there are no existing techniques for quickly detecting large-variance or large-gap clones in large codebases. In this paper, we propose a scalable clone detection technique that can detect large-variance clones from large codebases and describe its implementation, called NIL. NIL is a token-based clone detector that efficiently identifies clone candidates using an N-gram representation of token sequences and an inverted index. Then, NIL verifies the clone candidates by measuring their similarity based on the longest common subsequence between their token sequences. We evaluate NIL in terms of large-variance clone detection accuracy, general Type-1, Type-2, and Type-3 clone detection accuracy, and scalability. Our experimental results show that NIL has higher accuracy in terms of large-variance clone detection, equivalent accuracy in terms of general clone detection, and the shortest execution time for inputs of various sizes (1–250 MLOC) compared to existing state-of-the-art tools.

トップカンファレンス・トップ論文誌特別講演（PPL） 9/1 【16:50～18:05】

• 池渕 未来（国立情報学研究所）
  講演タイトル: 「Certifying Derivation of State Machines from Coroutines」
  発表会議名: POPL 2022
  講演概要: One of the biggest implementation challenges in security-critical network protocols is nested state machines. In practice today, state machines are either implemented manually at a low level, risking bugs easily missed in audits; or are written using higher-level abstractions like threads, depending on runtime systems that may sacrifice performance or compatibility with the ABIs of important platforms (e.g., resource-constrained IoT systems). We present a compiler-based technique allowing the best of both worlds, coding protocols in a natural high-level form, using freer monads to represent nested coroutines, which are then compiled automatically to lower-level code with explicit state. In fact, our compiler is implemented as a tactic in the Coq proof assistant, structuring compilation as search for an equivalence proof for source and target programs. As such, it is straightforwardly (and soundly) extensible with new hints, for instance regarding new data structures that may be used for efficient lookup of coroutines. As a case study, we implemented a core of TLS sufficient for use with popular Web browsers, and our experiments show that the extracted Haskell code achieves reasonable performance.

• 郡 茉友子（総合研究大学院大学）
  講演タイトル: 「The Lattice-Theoretic Essence of Property Directed Reachability Analysis」
  発表会議名: CAV 2022
  講演概要: We present LT-PDR, a lattice-theoretic generalization of Bradley’s property directed reachability analysis (PDR) algorithm. LT-PDR identifies the essence of PDR to be an ingenious combination of verification and refutation attempts based on the Knaster-Tarski and Kleene theorems. We introduce four concrete instances of LT-PDR, derive their implementation from a generic Haskell implementation of LT-PDR, and experimentally evaluate them. We also present a categorical structural theory that derives these instances.

座長: 中野 圭介 (東北大学)