Write a Blog >>
APLAS 2020
Mon 30 November - Wed 2 December 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:

https://aplas2020.hotcrp.com

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.

Dates
You're viewing the program in a time zone which is different from your device's time zone - change time zone

Conference Day
Mon 30 Nov

Displayed time zone: Osaka, Sapporo, Tokyo change

15:30 - 17:00
Debugging, Profiling and Constraint SolvingResearch Papers at online
Chair(s): Tachio TerauchiWaseda University
15:30
30m
Talk
A Counterexample-Guided Debugger for Non-Recursive Datalog
Research Papers
Van-Dang TranNational Institute of Informatics, Japan, Hiroyuki KatoNational Institute of Informatics, Japan, Zhenjiang HuPeking University
16:00
30m
Talk
A Symbolic Algorithm for the Case-Split Rule in String Constraint Solving
Research Papers
Yu-Fang ChenAcademia Sinica, Taiwan, Vojtěch HavlenaBrno University of Technology, Ondřej LengálBrno University of Technology, Andrea TurriniState Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences
16:30
30m
Talk
P3: A Profiler Suite for Parallel Applications on the Java Virtual Machine (Tool Paper)
Research Papers
Andrea RosàUniversity of Lugano, Switzerland, Walter BinderUniversity of Lugano, Switzerland
17:30 - 19:30
TypesResearch Papers at online
Chair(s): Marco ServettoVictoria University Wellington, New Zealand
17:30
30m
Talk
Syntactically Restricting Bounded Polymorphism for Decidable Subtyping
Research Papers
Julian MackayVictoria University of Wellington, Alex PotaninVictoria University of Wellington, Jonathan AldrichCarnegie Mellon University, Lindsay GrovesVictoria University of Wellington
18:00
30m
Talk
A New Refinement Type System for Automated nu-HFLZ Validity Checking
Research Papers
Hiroyuki KatsuraThe University of Tokyo, Naoki IwayamaUniversity of Tokyo, Japan, Naoki KobayashiUniversity of Tokyo, Japan, Takeshi TsukadaChiba University, Japan
18:30
30m
Talk
Behavioural Types for Memory and Method Safety in a Core Object-Oriented Language
Research Papers
Mario BravettiUniversità di Bologna, Adrian FrancalanzaUniversity of Malta, Iaroslav GolovanovDepartment of Computer Science, Aalborg University, Hans HüttelDepartment of Computer Science, Aalborg University, Mathias Steen JakobsenDepartment of Computer Science, Aalborg University, Denmark, Mikkel Klinke KettunenDepartment of Computer Science, Aalborg University, Denmark, Antonio RavaraDepartment of Informatics, Faculty of Sciences and Technology, NOVA University of Lisbon and NOVA LINCS
19:00
30m
Talk
Neural Networks, Secure by Construction: An Exploration of Refinement Types
Research Papers
Wen KokkeUniversity of Edinburgh, Ekaterina KomendantskayaHeriot-Watt University, UK, Daniel KienitzHeriot-Watt University, David AspinallUniversity of Edinburgh, Robert AtkeyUniversity of Strathclyde

Conference Day
Tue 1 Dec

Displayed time zone: Osaka, Sapporo, Tokyo change

10:30 - 12:00
Program Analysis and VerificationResearch Papers at online
Chair(s): Benjamin DelawarePurdue University
10:30
30m
Talk
Declarative Stream Runtime Verification (hLola)
Research Papers
Martin CeresaUNR - CIFASIS - CONICET, Felipe GorostiagaIMDEA Software Institute, César SánchezIMDEA Software Institute
11:00
30m
Talk
A Set-Based Context Model for Program Analysis
Research Papers
Zachary PalmerSwarthmore College, Scott F. SmithThe Johns Hopkins University, Leandro FacchinettiThe Johns Hopkins University, Ayaka YorihiroCornell University, Ke WuJohns Hopkins University
11:30
30m
Talk
Formal Verification of Atomicity Requirements for Smart Contracts
Research Papers
Ning HanCapital Normal University, Ximeng LiCapital Normal University, Guohui WangCapital Normal University, Beijing, China, Zhiping ShiCapital Normal University, Yong GuanCapital Normal University, Beijing, China
16:00 - 17:30
Program Generation, Transactions and AutomationResearch Papers at online
Chair(s): Shigeru ChibaThe University of Tokyo
16:00
30m
Talk
Automatically Generating Descriptive Texts in Logging Statements: How Far Are We?
Research Papers
Xiaotong LiuSchool of Software and Microelectronics, Peking University, Beijing, China, Tong JiaSchool of Software and Microelectronics, Peking University, Beijing, China, Ying LiSchool of Software and Microelectronics, Peking University, Beijing, China, Hao YuPeking University, Yang YueUniversity of California, Irvine, Chuanjia HouSchool of Software and Microelectronics, Peking University, Beijing, China
16:30
30m
Talk
Banyan: Coordination-free Transactions over Mergeable Replicated Data Types
Research Papers
Shashank Shekhar DubeyIIT Madras, KC SivaramakrishnanIIT Madras, Thomas GazagnaireTarides, Anil MadhavapeddyUniversity of Cambridge
17:00
30m
Talk
Stack-Driven Program Generation of WebAssembly
Research Papers
Árpád PerényiUniversity of Southern Denmark, Jan MidtgaardUniversity of Southern Denmark

Conference Day
Wed 2 Dec

Displayed time zone: Osaka, Sapporo, Tokyo change

15:30 - 17:00
Synthesis and Program TransformationResearch Papers at online
Chair(s): Cristina DavidUniversity of Oxford
15:30
30m
Talk
Relational Synthesis for Pattern Matching
Research Papers
Dmitrii Kosarev, Dmitri BoulytchevSaint Petersburg State University / JetBrains Research
16:00
30m
Talk
Parameterized Synthesis with Safety Properties
Research Papers
Oliver MarkgrafTechnische Universität Kaiserslautern, Anthony Widjaja LinTechnische Universität Kaiserslautern, Daniel NeiderMax Planck Institute for Software Systems, Muhammad NajibTechnische Universität Kaiserslautern, Chih-Duo HongUniversity of Oxford
16:30
30m
Talk
REFINITY to Model and Prove Program Transformation Rules
Research Papers
Dominic SteinhöfelTechnical University of Darmstadt
17:30 - 19:00
SemanticsResearch Papers at online
Chair(s): Florian Rabe University of Erlangen
17:30
30m
Talk
Certified Semantics for Relational Programming
Research Papers
Dmitry RozplokhasHigher School of Economics and JetBrains Research, Russia, Andrey VyatkinSaint Petersburg State University, Russia, Dmitri BoulytchevSaint Petersburg State University / JetBrains Research
18:00
30m
Talk
An Abstract Machine for Strong Call by Value
Research Papers
Malgorzata BiernackaUniversity of Wroclaw, Dariusz BiernackiUniversity of Wrocław, Witold CharatonikInstitute of Computer Science, University of Wroclaw, Tomasz DrabInstitute of Computer Science, University of Wroclaw
18:30
30m
Talk
Algebraic and coalgebraic perspectives on interaction laws
Research Papers
Tarmo UustaluReykjavik University, Niels VoorneveldTallinn University of Technology

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.

Accepted Papers

Title
A Counterexample-Guided Debugger for Non-Recursive Datalog
Research Papers
A New Refinement Type System for Automated nu-HFLZ Validity Checking
Research Papers
A Set-Based Context Model for Program Analysis
Research Papers
A Symbolic Algorithm for the Case-Split Rule in String Constraint Solving
Research Papers
Algebraic and coalgebraic perspectives on interaction laws
Research Papers
An Abstract Machine for Strong Call by Value
Research Papers
Automatically Generating Descriptive Texts in Logging Statements: How Far Are We?
Research Papers
Banyan: Coordination-free Transactions over Mergeable Replicated Data Types
Research Papers
Behavioural Types for Memory and Method Safety in a Core Object-Oriented Language
Research Papers
Certified Semantics for Relational Programming
Research Papers
Declarative Stream Runtime Verification (hLola)
Research Papers
Formal Verification of Atomicity Requirements for Smart Contracts
Research Papers
Neural Networks, Secure by Construction: An Exploration of Refinement Types
Research Papers
P3: A Profiler Suite for Parallel Applications on the Java Virtual Machine (Tool Paper)
Research Papers
Parameterized Synthesis with Safety Properties
Research Papers
REFINITY to Model and Prove Program Transformation Rules
Research Papers
Relational Synthesis for Pattern Matching
Research Papers
Stack-Driven Program Generation of WebAssembly
Research Papers
Syntactically Restricting Bounded Polymorphism for Decidable Subtyping
Research Papers