| 2019 | What's Wrong with On-the-Fly Partial Order Reduction. | Stephen F. Siegel |
| 2019 | Property Directed Self Composition. | Ron Shemer, Arie Gurfinkel, Sharon Shoham, Yakir Vizel |
| 2019 | Polytopic Trees for Verification of Learning-Based Controllers. | Sadra Sadraddini, Shen Shen, Osbert Bastani |
| 2019 | Abstraction Refinement Algorithms for Timed Automata. | Victor Roussanaly, Ocan Sankur, Nicolas Markey |
| 2019 | High-Level Abstractions for Simplifying Extended String Constraints in SMT. | Andrew Reynolds, Andres Ntzli, Clark W. Barrett, Cesare Tinelli |
| 2019 | cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis. | Andrew Reynolds, Haniel Barbosa, Andres Ntzli, Clark W. Barrett, Cesare Tinelli |
| 2019 | Incremental Determinization for Quantifier Elimination and Functional Synthesis. | Markus N. Rabe |
| 2019 | Overfitting in Synthesis: Theory and Practice. | Saswat Padhi, Todd D. Millstein, Aditya V. Nori, Rahul Sharma |
| 2019 | STAMINA: STochastic Approximate Model-Checker for INfinite-State Analysis. | Thakur Neupane, Chris J. Myers, Curtis Madsen, Hao Zheng, Zhen Zhang |
| 2019 | Automated Parameterized Verification of CRDTs. | Kartik Nagar, Suresh Jagannathan |
| 2019 | Satisfiability Checking for Mission-Time LTL. | Jianwen Li, Moshe Y. Vardi, Kristin Y. Rozier |
| 2019 | Formal Verification of Quantum Algorithms Using Quantum Hoare Logic. | Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying, Naijun Zhan |
| 2019 | Verifying Asynchronous Event-Driven Programs Using Partial Abstract Transformers. | Peizun Liu, Thomas Wahl, Akash Lal |
| 2019 | AliveInLean: A Verified LLVM Peephole Optimization Verifier. | Juneyoung Lee, Chung-Kil Hur, Nuno P. Lopes |
| 2019 | Approximate Probabilistic Relations for Compositional Abstractions of Stochastic Systems. | Abolfazl Lavaei, Sadegh Soudjani, Majid Zamani |
| 2019 | Cerberus-BMC: A Principled Reference Semantics and Exploration Tool for Concurrent and Sequential C. | Stella Lau, Victor B. F. Gomes, Kayvan Memarian, Jean Pichon-Pharabod, Peter Sewell |
| 2019 | Verifying Asynchronous Interactions via Communicating Session Automata. | Julien Lange, Nobuko Yoshida |
| 2019 | Interpolating Strong Induction. | Hari Govind Vediramana Krishnan, Yakir Vizel, Vijay Ganesh, Arie Gurfinkel |
| 2019 | Clock Bound Repair for Timed Systems. | Martin Klbl, Stefan Leue, Thomas Wies |
| 2019 | Flexible Computational Pipelines for Robust Abstraction-Based Control Synthesis. | Eric S. Kim, Murat Arcak, Sanjit A. Seshia |
| 2019 | The Marabou Framework for Verification and Analysis of Deep Neural Networks. | Guy Katz, Derek A. Huang, Duligur Ibeling, Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, Aleksandar Zeljic, David L. Dill, Mykel J. Kochenderfer, Clark W. Barrett |
| 2019 | Automated Synthesis of Secure Platform Mappings. | Eunsuk Kang, Stphane Lafortune, Stavros Tripakis |
| 2019 | Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors. | Martin Jons, Jan Strejcek |
| 2019 | Trust, Resilience and Interpretability of AI Models. | Susmit Jha |
| 2019 | Local and Compositional Reasoning for Optimized Reactive Systems. | Mitesh Jain, Panagiotis Manolios |