Research PapersAPLAS 2019
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 EasyChair (see Submission Information). 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.
Mon 2 DecDisplayed time zone: Beijing, Chongqing, Hong Kong, Urumqi change
08:50 - 10:00 | Keynote 1Keynote Talks at Bali Room Chair(s): Anthony Widjaja Lin Technische Universität Kaiserslautern | ||
08:50 70mTalk | Proving that Programs are Differentially Private Keynote Talks |
10:00 - 10:30 | Coffee BreakCatering | ||
10:30 - 12:00 | |||
10:30 30mTalk | Manifest Contracts with Intersection Types Research Papers Pre-print | ||
11:00 30mTalk | A Dependently Typed Multi-Stage Calculus Research Papers Pre-print | ||
11:30 30mTalk | Existential Types for Relaxed Noninterference Research Papers |
12:00 - 13:30 | |||
13:30 - 15:00 | |||
13:30 30mTalk | Dissecting Widening: Separating Termination from Information Research Papers Graeme Gange , Jorge A. Navas SRI International, Peter Schachte , Harald Sondergaard , Peter J. Stuckey Monash University | ||
14:00 30mTalk | A Type-Based HFL Model Checking Algorithm Research Papers Youkichi Hosoi The University of Tokyo , Naoki Kobayashi University of Tokyo, Japan, Takeshi Tsukada University of Tokyo, Japan | ||
14:30 30mTalk | Reducing Static Analysis Alarms based on Non-impacting Control Dependencies Research Papers Tukaram Muske Tata Consultancy Services Ltd, Rohith Talluri Tata Consultancy Services Ltd, Alexander Serebrenik Eindhoven University of Technology |
15:00 - 15:30 | Coffee BreakCatering | ||
15:30 - 17:00 | |||
15:30 30mTalk | Factorization and Normalization, Essentially Research Papers Beniamino Accattoli Inria & Ecole Polytechnique, Claudia Faggian IRIF, Giulio Guerrieri University of Bath | ||
16:00 30mTalk | Formal Verifications of Call-by-Need and Call-by-Name Evaluations with Mutual Recursion Research Papers | ||
16:30 30mTalk | Recursion Schemes in Coq Research Papers |
18:00 - 20:00 | |||
18:00 - 20:00 | Poster sessionPosters at Puri Bali Chair(s): Andreea Costea School of Computing, National University Of Singapore | ||
Tue 3 DecDisplayed time zone: Beijing, Chongqing, Hong Kong, Urumqi change
10:00 - 10:30 | Coffee BreakCatering | ||
10:30 - 12:00 | Language Design and ImplementationResearch Papers at Bali Room Chair(s): Sandrine Blazy Univ Rennes- IRISA | ||
10:30 30mTalk | Lightweight Functional Logic Meta-Programming Research Papers Nada Amin Harvard University, William E. Byrd University of Alabama at Birmingham, USA, Tiark Rompf Purdue University | ||
11:00 30mTalk | Mimalloc: Free List Sharding in Action Research Papers | ||
11:30 30mTalk | LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL Research Papers Yutaka Nagashima Data61, Australia |
12:00 - 13:30 | |||
13:30 - 15:00 | |||
13:30 30mTalk | Android Multitasking Mechanism: Formal Semantics and Static Analysis of Apps Research Papers Taolue Chen Birkbeck, University of London, Jilong He Institute of Software, Chinese Academy of Sciences, Yu-Ping Wang Tsinghua University, China, Zhilin Wu State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Jun Yan Institute of Software, Chinese Academy of Sciences | ||
14:00 30mTalk | Conflict Abstractions and Shadow Speculation for Optimistic Transactional Objects Research Papers Thomas Dickerson Brown University, Paul Gazzillo University of Central Florida, Maurice Herlihy Brown University, USA, Eric Koskinen Stevens Institute of Technology | ||
14:30 30mTalk | Transactional Forest: A DSL for Managing Concurrent Filestores Research Papers Jonathan DiLorenzo Cornell University, Kathryn Mancini Cornell University, Kathleen Fisher Tufts University, USA, Nate Foster Cornell University |
15:00 - 15:30 | Coffee BreakCatering | ||
15:30 - 17:15 | VerificationResearch Papers at Bali Room Chair(s): Zhilin Wu State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences | ||
15:30 15mTalk | J-ReCoVer: Java Reducer Commutativity Verifier [Tool Paper] Research Papers Yu-Fang Chen Academia Sinica, Chang-Yi Chiang Graduate Institute of Information Management, National Taipei University, Taiwan, Lukáš Holík Brno University of Technology, Wei-Tsung Kao Institute of Information Science, Academia Sinica, Taiwan, Hsin-Hung Lin Institute of Information Science, Academia Sinica, Taiwan, Yean-Fu Wen Graduate Institute of Information Management, National Taipei University, Taiwan, Tomáš Vojnar Brno University of Technology, Wei-Cheng Wu Institute of Information Science, Academia Sinica, Taiwan | ||
15:45 30mTalk | Uniform Random Process Model Revisited Research Papers Wenbo Zhang , Huan Long Shanghai Jiao Tong University, Xian Xu East China University of Science and Technology | ||
16:15 30mTalk | Completeness of Cyclic Proofs for Symbolic Heaps with Inductive Definitions Research Papers Makoto Tatsuta National Institute of Informatics, Koji Nakazawa Graduate School of Informatics, Nagoya University, Daisuke Kimura Toho University | ||
16:45 30mTalk | Compositional Verification of Heap-Manipulating Programs through Property-Guided Learning Research Papers Long H. Pham Singapore University of Technology and Design, Jun Sun Singapore Management University, Singapore, Quang Loc Le Teesside University |
18:00 - 21:00 | |||
Wed 4 DecDisplayed time zone: Beijing, Chongqing, Hong Kong, Urumqi change
10:00 - 10:30 | Coffee BreakCatering | ||
10:30 - 12:00 | Logic and AutomataResearch Papers at Bali Room Chair(s): Peter Thiemann University of Freiburg, Germany | ||
10:30 30mTalk | Pumping, With or Without Choice Research Papers Aquinas Hobor National University of Singapore, Singapore, Elaine Li Runtime Verification, Inc., Frank Stephan National University of Singapore | ||
11:00 30mTalk | Simulations in Rank-Based Buchi Automata Complementation Research Papers Yu-Fang Chen Academia Sinica, Vojtěch Havlena Brno University of Technology, Ondřej Lengál Brno University of Technology | ||
11:30 30mTalk | Succinct Determinisation of Counting Automata via Sphere Construction Research Papers Lukáš Holík Brno University of Technology, Tomáš Vojnar Brno University of Technology, Ondřej Lengál Brno University of Technology , Lenka Turoňová Brno University of Technology, Margus Veanes Microsoft Research, Olli Saarikivi |
12:00 - 13:30 | |||
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.
Submission Information
Papers should be submitted electronically via the submission web page using EasyChair. 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 2019 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 anonymized, 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.
Tool papers
To facilitate the reviewing process, tool papers should clearly be so indicated in the EasyChair submission. We strongly recommend that the authors add the suffix ‘[Tool Paper]’ to the title of the submission in the EasyChair, but not necessarily in the paper itself.
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.