Research PapersAPLAS 2020
We solicit contributions in the forms of regular research papers, and tool papers. Among others, solicited topics include:
- Semantics, logics, foundational theory
- Design of languages, type systems, and foundational calculi
- Domain-specific languages
- Compilers, interpreters, abstract machines
- Program derivation, synthesis, and transformation
- Program analysis, verification, model-checking
- Logic, constraint, probabilistic, and quantum programming
- Software security
- Concurrency and parallelism
- Tools and environments for programming and implementation
- Applications of SAT/SMT to programming and implementation
Papers should be submitted electronically via the submission web page using HotCRP:
The acceptable format is PDF. Submitted papers must be unpublished and not submitted for publication elsewhere. Papers must be written in English. The proceedings will be published as a volume in Springer’s LNCS series. Accepted papers must be presented at the conference.
REVIEW PROCESS
APLAS 2020 will use a lightweight double-blind reviewing process. Following this process means that reviewers will not see the authors’ names or affiliations as they initially review a paper. The authors’ names will then be revealed to the reviewers only once their reviews have been submitted. To facilitate this process, submitted papers must adhere to the following: Author names and institutions must be omitted and References to the authors’ own related work should be in the third person (e.g., not “We build on our previous work …” but rather “We build on the work of …”). The purpose of this process is to help the reviewers come to an initial judgement about the paper without bias, not to make it impossible for them to discover the authors if they were to try. Nothing should be done in the name of anonymity that weakens the submission, makes the job of reviewing the paper more difficult, or interferes with the process of disseminating new ideas. For example, important background references should not be omitted or anonymised, even if they are written by the same authors and share common ideas, techniques, or infrastructure. Authors should feel free to disseminate their ideas or draft versions of their paper as they normally would. For instance, authors may post drafts of their papers on the web or give talks on their research ideas.
AUTHOR RESPONSE PERIOD
During the author response period, authors will be able to read reviews and respond to them as appropriate.
RESEARCH INTEGRITY
The Program Committee reserves the right, up until the time of publication, to reverse a decision of paper acceptance. Reversal is possible if fatal flaws are discovered in the paper, or research integrity is found to have been seriously breached.
Mon 30 NovDisplayed time zone: Osaka, Sapporo, Tokyo change
15:30 - 17:00 | Debugging, Profiling and Constraint SolvingResearch Papers at online Chair(s): Tachio Terauchi Waseda University | ||
15:30 30mTalk | A Counterexample-Guided Debugger for Non-Recursive Datalog Research Papers Van-Dang Tran National Institute of Informatics, Japan, Hiroyuki Kato National Institute of Informatics, Japan, Zhenjiang Hu Peking University | ||
16:00 30mTalk | A Symbolic Algorithm for the Case-Split Rule in String Constraint Solving Research Papers Yu-Fang Chen Academia Sinica, Taiwan, Vojtěch Havlena Brno University of Technology, Ondřej Lengál Brno University of Technology, Andrea Turrini State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences | ||
16:30 30mTalk | P3: A Profiler Suite for Parallel Applications on the Java Virtual Machine (Tool Paper) Research Papers | ||
17:30 - 19:30 | |||
17:30 30mTalk | Syntactically Restricting Bounded Polymorphism for Decidable Subtyping Research Papers Julian Mackay Victoria University of Wellington, Alex Potanin Victoria University of Wellington, Jonathan Aldrich Carnegie Mellon University, Lindsay Groves Victoria University of Wellington | ||
18:00 30mTalk | A New Refinement Type System for Automated nu-HFLZ Validity Checking Research Papers Hiroyuki Katsura The University of Tokyo, Naoki Iwayama University of Tokyo, Japan, Naoki Kobayashi University of Tokyo, Japan, Takeshi Tsukada Chiba University, Japan | ||
18:30 30mTalk | Behavioural Types for Memory and Method Safety in a Core Object-Oriented Language Research Papers Mario Bravetti Università di Bologna, Adrian Francalanza University of Malta, Iaroslav Golovanov Department of Computer Science, Aalborg University, Hans Hüttel Department of Computer Science, Aalborg University, Mathias Steen Jakobsen Department of Computer Science, Aalborg University, Denmark, Mikkel Klinke Kettunen Department of Computer Science, Aalborg University, Denmark, António Ravara Department of Informatics, Faculty of Sciences and Technology, NOVA University of Lisbon and NOVA LINCS | ||
19:00 30mTalk | Neural Networks, Secure by Construction: An Exploration of Refinement Types Research Papers Wen Kokke University of Edinburgh, Ekaterina Komendantskaya Heriot-Watt University, UK, Daniel Kienitz Heriot-Watt University, David Aspinall University of Edinburgh, Robert Atkey University of Strathclyde | ||
Tue 1 DecDisplayed time zone: Osaka, Sapporo, Tokyo change
10:30 - 12:00 | Program Analysis and VerificationResearch Papers at online Chair(s): Benjamin Delaware Purdue University | ||
10:30 30mTalk | Declarative Stream Runtime Verification (hLola) Research Papers Martin Ceresa UNR - CIFASIS - CONICET, Felipe Gorostiaga IMDEA Software Institute, César Sánchez IMDEA Software Institute | ||
11:00 30mTalk | A Set-Based Context Model for Program Analysis Research Papers Zachary Palmer Swarthmore College, Scott F. Smith The Johns Hopkins University, Leandro Facchinetti The Johns Hopkins University, Ayaka Yorihiro Cornell University, Ke Wu Johns Hopkins University | ||
11:30 30mTalk | Formal Verification of Atomicity Requirements for Smart Contracts Research Papers Ning Han Capital Normal University, Ximeng Li Capital Normal University, Guohui Wang Capital Normal University, Beijing, China, Zhiping Shi Capital Normal University, Yong Guan Capital Normal University, Beijing, China | ||
16:00 - 17:30 | Program Generation, Transactions and AutomationResearch Papers at online Chair(s): Shigeru Chiba The University of Tokyo | ||
16:00 30mTalk | Automatically Generating Descriptive Texts in Logging Statements: How Far Are We? Research Papers Xiaotong Liu School of Software and Microelectronics, Peking University, Beijing, China, Tong Jia School of Software and Microelectronics, Peking University, Beijing, China, Ying Li School of Software and Microelectronics, Peking University, Beijing, China, Hao Yu Peking University, Yang Yue University of California, Irvine, Chuanjia Hou School of Software and Microelectronics, Peking University, Beijing, China | ||
16:30 30mTalk | Banyan: Coordination-free Transactions over Mergeable Replicated Data Types Research Papers Shashank Shekhar Dubey IIT Madras, KC Sivaramakrishnan IIT Madras, Thomas Gazagnaire Tarides, Anil Madhavapeddy University of Cambridge | ||
17:00 30mTalk | Stack-Driven Program Generation of WebAssembly Research Papers | ||
Wed 2 DecDisplayed time zone: Osaka, Sapporo, Tokyo change
15:30 - 17:00 | Synthesis and Program TransformationResearch Papers at online Chair(s): Cristina David University of Oxford | ||
15:30 30mTalk | Relational Synthesis for Pattern Matching Research Papers | ||
16:00 30mTalk | Parameterized Synthesis with Safety Properties Research Papers Oliver Markgraf Technische Universität Kaiserslautern, Anthony Widjaja Lin Technische Universität Kaiserslautern, Daniel Neider Max Planck Institute for Software Systems, Muhammad Najib Technische Universität Kaiserslautern, Chih-Duo Hong University of Oxford | ||
16:30 30mTalk | REFINITY to Model and Prove Program Transformation Rules Research Papers Dominic Steinhöfel Technical University of Darmstadt | ||
17:30 - 19:00 | |||
17:30 30mTalk | Certified Semantics for Relational Programming Research Papers Dmitry Rozplokhas Higher School of Economics and JetBrains Research, Russia, Andrey Vyatkin Saint Petersburg State University, Russia, Dmitri Boulytchev Saint Petersburg State University / JetBrains Research | ||
18:00 30mTalk | An Abstract Machine for Strong Call by Value Research Papers Malgorzata Biernacka University of Wroclaw, Dariusz Biernacki University of Wrocław, Witold Charatonik Institute of Computer Science, University of Wroclaw, Tomasz Drab Institute of Computer Science, University of Wroclaw Link to publication | ||
18:30 30mTalk | Algebraic and coalgebraic perspectives on interaction laws Research Papers | ||
Accepted Papers
Call for Tool Papers
We solicit submissions in the form of tool papers describing a demonstration of a tool or a system that support theory, program construction, reasoning, or program execution in the scope of APLAS. The main purpose of a tool paper is to display a completed, robust and well-documented tool-highlighting the overall functionality of the tool, the interfaces of the tool, interesting examples and applications of the tool, an assessment of the tool’s strengths and weaknesses, and a summary of documentation/support available with the tool. Authors of tool demonstration proposals are expected to present a live demonstration of the tool at the conference. It is highly desirable that the tools are available on the web. System and Tool papers should not exceed 8 pages in the Springer LNCS format, including bibliography and figures. They may include an additional appendix of up to 6 extra pages giving the outline, screenshots, examples, etc. to indicate the content of the proposed live demo.
Call for Regular Research Papers
We solicit submissions in the form of regular research papers describing original scientific research results, including system development and case studies. Among others, solicited topics include:
- Semantics, logics, foundational theory
- Design of languages, type systems, and foundational calculi
- Domain-specific languages
- Compilers, interpreters, abstract machines
- Program derivation, synthesis, and transformation
- Program analysis, verification, model-checking
- Logic, constraint, probabilistic, and quantum programming
- Software security
- Concurrency and parallelism
- Tools and environments for programming and implementation
- Applications of SAT/SMT to programming and implementation
Regular research papers should not exceed 18 pages in the Springer LNCS format, including bibliography and figures. This category encompasses both theoretical and implementation (also known as system descriptions) papers. In either case, submissions should clearly identify what has been accomplished and why it is significant. Submissions will be judged on the basis of significance, relevance, correctness, originality, and clarity. System descriptions papers should contain a link to a working system and will be judged on originality, usefulness, and design. In case of lack of space, proofs, experimental results, or any information supporting the technical results of the paper could be provided as an appendix or a link to a web page, but reviewers are not obliged to read them.