| 2019 | Alternating Automata Modulo First Order Theories. | Radu Iosif, Xiao Xu |
| 2019 | Proving Unrealizability for Syntax-Guided Synthesis. | Qinheping Hu, Jason Breck, John Cyphert, Loris D'Antoni, Thomas W. Reps |
| 2019 | Evaluating Branching Heuristics in Interval Constraint Propagation for Satisfiability. | Calvin Huang, Soonho Kong, Sicun Gao, Damien Zufferey |
| 2019 | Probabilistic Bisimulation for Parameterized Systems - (with Applications to Verifying Anonymous Protocols). | Chih-Duo Hong, Anthony W. Lin, Rupak Majumdar, Philipp Rmmer |
| 2019 | Stochastic Local Search for Solving Floating-Point Constraints. | Shaobo He, Marek S. Baranowski, Zvonimir Rakamaric |
| 2019 | Integrating Formal Schedulability Analysis into a Verified OS Kernel. | Xiaojie Guo, Maxime Lesourd, Mengqi Liu, Lionel Rieg, Zhong Shao |
| 2019 | Efficient Verification of Network Fault Tolerance via Counterexample-Guided Refinement. | Nick Giannarakis, Ryan Beckett, Ratul Mahajan, David Walker |
| 2019 | Rigorous Continuous Evolution of Uncertain Systems. | Luca Geretti, Sanja Zivanovic Gonzalez, Pieter Collins, Davide Bresolin, Tiziano Villa |
| 2019 | BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings. | Natalia Gavrilenko, Hernn Ponce de Len, Florian Furbach, Keijo Heljanko, Roland Meyer |
| 2019 | Fast Algorithms for Handling Diagonal Constraints in Timed Automata. | Paul Gastin, Sayan Mukherjee, B. Srivathsan |
| 2019 | Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems. | Sicun Gao, James Kapinski, Jyotirmoy V. Deshmukh, Nima Roohi, Armando Solar-Lezama, Nikos Archiga, Soonho Kong |
| 2019 | Termination of Triangular Integer Loops is Decidable. | Florian Frohn, Jrgen Giesl |
| 2019 | Temporal Stream Logic: Synthesis Beyond the Bools. | Bernd Finkbeiner, Felix Klein, Ruzica Piskac, Mark Santolucito |
| 2019 | Taming Delays in Dynamical Systems - Unbounded Verification of Delay Differential Equations. | Shenghua Feng, Mingshuai Chen, Naijun Zhan, Martin Frnzle, Bai Xue |
| 2019 | Inferring Inductive Invariants from Phase Structures. | Yotam M. Y. Feldman, James R. Wilcox, Sharon Shoham, Mooly Sagiv |
| 2019 | Quantified Invariants via Syntax-Guided Synthesis. | Grigory Fedyukovich, Sumanth Prabhu, Kumar Madhukar, Aarti Gupta |
| 2019 | StreamLAB: Stream-based Monitoring of Cyber-Physical Systems. | Peter Faymonville, Bernd Finkbeiner, Malte Schledjewski, Maximilian Schwenger, Marvin Stenger, Leander Tentrup, Hazem Torfah |
| 2019 | Automated Hypersafety Verification. | Azadeh Farzan, Anthony Vandikas |
| 2019 | SecCSL: Security Concurrent Separation Logic. | Gidon Ernst, Toby Murray |
| 2019 | Violat: Generating Tests of Observational Refinement for Concurrent Objects. | Michael Emmi, Constantin Enea |
| 2019 | Security-Aware Synthesis Using Delayed-Action Games. | Mahmoud Elfar, Yu Wang, Miroslav Pajic |
| 2019 | Efficient Synthesis with Probabilistic Constraints. | Samuel Drews, Aws Albarghouthi, Loris D'Antoni |
| 2019 | VerifAI: A Toolkit for the Formal Design and Analysis of Artificial Intelligence-Based Systems. | Tommaso Dreossi, Daniel J. Fremont, Shromona Ghosh, Edward Kim, Hadi Ravanbakhsh, Marcell Vazquez-Chanlatte, Sanjit A. Seshia |
| 2019 | Synthesizing Approximate Implementations for Unrealizable Specifications. | Rayna Dimitrova, Bernd Finkbeiner, Hazem Torfah |
| 2019 | An Evaluation of Monte-Carlo Tree Search for Property Falsification on Hybrid Flight Control Laws. | Rmi Delmas, Thomas Loquen, Josep Boada-Bauxell, Mathieu Carton |