| 2017 | GPUDrano: Detecting Uncoalesced Accesses in GPU Programs. | Rajeev Alur, Joseph Devietti, Omar S. Navarro Leija, Nimit Singhania |
| 2017 | Quantitative Assume Guarantee Synthesis. | Shaull Almagor, Orna Kupferman, Jan Oliver Ringert, Yaron Velner |
| 2017 | Context-Sensitive Dynamic Partial Order Reduction. | Elvira Albert, Puri Arenas, Maria Garcia de la Banda, Miguel Gmez-Zamalloa, Peter J. Stuckey |
| 2017 | Repairing Decision-Making Programs Under Uncertainty. | Aws Albarghouthi, Loris D'Antoni, Samuel Drews |
| 2017 | Classification and Coverage-Based Falsification for Embedded Control Systems. | Arvind S. Adimoolam, Thao Dang, Alexandre Donz, James Kapinski, Xiaoqing Jin |
| 2017 | Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants. | Alessandro Abate, Iury Bessa, Dario Cattaruzza, Lucas C. Cordeiro, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen |
| 2016 | A Practical Verification Framework for Preemptive OS Kernels. | Fengwei Xu, Ming Fu, Xinyu Feng, Xiaoran Zhang, Hui Zhang, Zhaohui Li |
| 2016 | Under-Approximating Backward Reachable Sets by Polytopes. | Bai Xue, Zhikun She, Arvind Easwaran |
| 2016 | BFS-Based Model Checking of Linear-Time Properties with an Application on GPUs. | Anton Wijs |
| 2016 | String Analysis via Automata Manipulation with Logic Circuit Representation. | Hung-En Wang, Tzung-Lin Tsai, Chun-Han Lin, Fang Yu, Jie-Hong R. Jiang |
| 2016 | Progressive Reasoning over Recursively-Defined Strings. | Minh-Thai Trinh, Duc-Hiep Chu, Joxan Jaffar |
| 2016 | Limit-Deterministic Bchi Automata for Linear Temporal Logic. | Salomon Sickert, Javier Esparza, Stefan Jaax, Jan Kretnsk |
| 2016 | BigraphER: Rewriting and Analysis Engine for Bigraphs. | Michele Sevegnani, Muffy Calder |
| 2016 | Reduce the Complexity of the Polyhedron Minimization Using the Max Plus Pruning Method. | Yassamine Seladji |
| 2016 | Probabilistic Automated Language Learning for Configuration Files. | Mark Santolucito, Ennan Zhai, Ruzica Piskac |
| 2016 | Model Based Automatic Code Generation for Nonlinear Model Predictive Control. | Behzad Samadi |
| 2016 | End-to-End Verification of Processors with ISA-Formal. | Alastair Reid, Rick Chen, Anastasios Deligiannis, David Gilday, David Hoyes, Will Keen, Ashan Pathirane, Owen Shepherd, Peter Vrabel, Ali Zaidi |
| 2016 | Counterexample Guided Abstraction Refinement for Stability Analysis. | Pavithra Prabhakar, Miriam Garcia Soto |
| 2016 | Investigating Safety of a Radiotherapy Machine Using System Models with Pluggable Checkers. | Stuart Pernsteiner, Calvin Loncaric, Emina Torlak, Zachary Tatlock, Xi Wang, Michael D. Ernst, Jonathan Jacky |
| 2016 | Precise and Complete Propagation Based Local Search for Satisfiability Modulo Theories. | Aina Niemetz, Mathias Preiner, Armin Biere |
| 2016 | PSCV: A Runtime Verification Tool for Probabilistic SystemC Models. | Van Chan Ngo, Axel Legay, Vania Joloboff |
| 2016 | From Shape Analysis to Termination Analysis in Linear Time. | Roman Manevich, Boris Dogadov, Noam Rinetzky |
| 2016 | Liveness of Randomised Parameterised Systems under Arbitrary Schedulers. | Anthony W. Lin, Philipp Rmmer |
| 2016 | Satisfiability Modulo Heap-Based Programs. | Quang Loc Le, Jun Sun, Wei-Ngan Chin |
| 2016 | Trigger Selection Strategies to Stabilize Program Verifiers. | K. Rustan M. Leino, Clment Pit-Claudel |