| 2020 | REFINITY to Model and Prove Program Transformation Rules. | Dominic Steinhfel |
| 2020 | Certified Semantics for Relational Programming. | Dmitry Rozplokhas, Andrey Vyatkin, Dmitry Boulytchev |
| 2020 | P | Andrea Ros, Walter Binder |
| 2020 | Stack-Driven Program Generation of WebAssembly. | rpd Pernyi, Jan Midtgaard |
| 2020 | Parameterized Synthesis with Safety Properties. | Oliver Markgraf, Chih-Duo Hong, Anthony W. Lin, Muhammad Najib, Daniel Neider |
| 2020 | Syntactically Restricting Bounded Polymorphism for Decidable Subtyping. | Julian Mackay, Alex Potanin, Jonathan Aldrich, Lindsay Groves |
| 2020 | Automatically Generating Descriptive Texts in Logging Statements: How Far Are We? | Xiaotong Liu, Tong Jia, Ying Li, Hao Yu, Yang Yue, Chuanjia Hou |
| 2020 | Relational Synthesis for Pattern Matching. | Dmitry Kosarev, Petr Lozov, Dmitry Boulytchev |
| 2020 | Neural Networks, Secure by Construction - An Exploration of Refinement Types. | Wen Kokke, Ekaterina Komendantskaya, Daniel Kienitz, Robert Atkey, David Aspinall |
| 2020 | A New Refinement Type System for Automated $\nu \text {HFL}_\mathbb {Z}$ Validity Checking. | Hiroyuki Katsura, Naoki Iwayama, Naoki Kobayashi, Takeshi Tsukada |
| 2020 | Formal Verification of Atomicity Requirements for Smart Contracts. | Ning Han, Ximeng Li, Guohui Wang, Zhiping Shi, Yong Guan |
| 2020 | A Set-Based Context Model for Program Analysis. | Leandro Facchinetti, Zachary Palmer, Scott F. Smith, Ke Wu, Ayaka Yorihiro |
| 2020 | Banyan: Coordination-Free Distributed Transactions over Mergeable Types. | Shashank Shekhar Dubey, K. C. Sivaramakrishnan, Thomas Gazagnaire, Anil Madhavapeddy |
| 2020 | A Symbolic Algorithm for the Case-Split Rule in String Constraint Solving. | Yu-Fang Chen, Vojtech Havlena, Ondrej Lengl, Andrea Turrini |
| 2020 | Declarative Stream Runtime Verification (hLola). | Martn Ceresa, Felipe Gorostiaga, Csar Snchez |
| 2020 | Behavioural Types for Memory and Method Safety in a Core Object-Oriented Language. | Mario Bravetti, Adrian Francalanza, Iaroslav Golovanov, Hans Httel, Mathias Jakobsen, Mikkel Kettunen, Antnio Ravara |
| 2020 | An Abstract Machine for Strong Call by Value. | Malgorzata Biernacka, Dariusz Biernacki, Witold Charatonik, Tomasz Drab |
| 2019 | Uniform Random Process Model Revisited. | Wenbo Zhang, Huan Long, Xian Xu |
| 2019 | Completeness of Cyclic Proofs for Symbolic Heaps with Inductive Definitions. | Makoto Tatsuta, Koji Nakazawa, Daisuke Kimura |
| 2019 | Compositional Verification of Heap-Manipulating Programs Through Property-Guided Learning. | Long H. Pham, Jun Sun, Quang Loc Le |
| 2019 | Manifest Contracts with Intersection Types. | Yuki Nishida, Atsushi Igarashi |
| 2019 | LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL. | Yutaka Nagashima |
| 2019 | Reducing Static Analysis Alarms Based on Non-impacting Control Dependencies. | Tukaram Muske, Rohith Talluri, Alexander Serebrenik |
| 2019 | Recursion Schemes in Coq. | Kosuke Murata, Kento Emoto |
| 2019 | Formal Verifications of Call-by-Need and Call-by-Name Evaluations with Mutual Recursion. | Masayuki Mizuno, Eijiro Sumii |