| 2020 | Action-Based Model Checking: Logic, Automata, and Reduction. | Stephen F. Siegel, Yihao Yan |
| 2020 | Populating the Peephole Optimizer of a Smart Contract Compiler. | Maria Anna Schett, Julian Nagele |
| 2020 | Symbolic Partial-Order Execution for Testing Multi-Threaded Programs. | Daniel Schemmel, Julian Bning, Csar Rodrguez, David Laprell, Klaus Wehrle |
| 2020 | Verification of Quantitative Hyperproperties Using Trace Enumeration Relations. | Shubham Sahai, Pramod Subramanyan, Rohit Sinha |
| 2020 | Mechanized Formal Model of Bitcoin's Blockchain Validation Procedures. | Kristijan Rupic, Lovro Rozic, Ante Derek |
| 2020 | Must Fault Localization for Program Repair. | Bat-Chen Rothenberg, Orna Grumberg |
| 2020 | Formal Design, Implementation and Verification of Blockchain Languages Using K (Invited Talk). | Grigore Rosu |
| 2020 | STMC: Statistical Model Checker with Stratified and Antithetic Sampling. | Nima Roohi, Yu Wang, Matthew West, Geir E. Dullerud, Mahesh Viswanathan |
| 2020 | Tezla, an Intermediate Representation for Static Analysis of Michelson Smart Contracts. | Joo Santos Reis, Paul Andrew Crocker, Simo Melo de Sousa |
| 2020 | Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic. | Azalea Raad, Josh Berdine, Hoang-Hai Dang, Derek Dreyer, Peter W. O'Hearn, Jules Villard |
| 2020 | Widest Paths and Global Propagation in Bounded Value Iteration for Stochastic Games. | Kittiphon Phalakarn, Toru Takisaka, Thomas Haas, Ichiro Hasuo |
| 2020 | Validation of Abstract Side-Channel Models for Computer Architectures. | Hamed Nemati, Pablo Buiras, Andreas Lindner, Roberto Guanciale, Swen Jacobs |
| 2020 | Semantics, Specification, and Bounded Verification of Concurrent Libraries in Replicated Systems. | Kartik Nagar, Prasita Mukherjee, Suresh Jagannathan |
| 2020 | Ivy: A Multi-modal Verification Tool for Distributed Algorithms. | Kenneth L. McMillan, Oded Padon |
| 2020 | On the Formal Verification of the Stellar Consensus Protocol. | Giuliano Losa, Mike Dodds |
| 2020 | Authenticated Data Structures as Functors in Isabelle/HOL. | Andreas Lochbihler, Ognjen Maric |
| 2020 | Hampa: Solver-Aided Recency-Aware Replication. | Xiao Li, Farzin Houshmand, Mohsen Lesani |
| 2020 | AMYTISS: Parallelized Automated Controller Synthesis for Large-Scale Stochastic Systems. | Abolfazl Lavaei, Mahmoud Khaled, Sadegh Soudjani, Majid Zamani |
| 2020 | PRISM-games 3.0: Stochastic Game Verification with Concurrency, Equilibria and Time. | Marta Kwiatkowska, Gethin Norman, David Parker, Gabriel Santos |
| 2020 | Decidable Synthesis of Programs with Uninterpreted Functions. | Paul Krogmeier, Umang Mathur, Adithya Murali, P. Madhusudan, Mahesh Viswanathan |
| 2020 | Global Guidance for Local Generalization in Model Checking. | Hari Govind Vediramana Krishnan, Yuting Chen, Sharon Shoham, Arie Gurfinkel |
| 2020 | Refinement for Structured Concurrent Programs. | Bernhard Kragl, Shaz Qadeer, Thomas A. Henzinger |
| 2020 | TarTar: A Timed Automata Repair Tool. | Martin Klbl, Stefan Leue, Thomas Wies |
| 2020 | Towards Model Checking Real-World Software-Defined Networks. | Vasileios Klimis, George Parisis, Bernhard Reus |
| 2020 | Inter-Blockchain Protocols with the Isabelle Infrastructure Framework. | Florian Kammller, Uwe Nestmann |