| 2016 | Reward-Bounded Reachability Probability for Uncertain Weighted MDPs. | Vahid Hashemi, Holger Hermanns, Lei Song |
| 2016 | Lazy Constrained Monotonic Abstraction. | Zeinab Ganjei, Ahmed Rezine, Petru Eles, Zebo Peng |
| 2016 | An Abstract Domain of Uninterpreted Functions. | Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Sndergaard, Peter J. Stuckey |
| 2016 | From Low-Level Pointers to High-Level Containers. | Kamil Dudka, Luks Holk, Petr Peringer, Marek Trtk, Toms Vojnar |
| 2016 | A Program Logic for C11 Memory Fences. | Marko Doko, Viktor Vafeiadis |
| 2016 | Parameter Synthesis for Parametric Interval Markov Chains. | Benot Delahaye, Didier Lime, Laure Petrucci |
| 2016 | Abstraction-driven Concolic Testing. | Przemyslaw Daca, Ashutosh Gupta, Thomas A. Henzinger |
| 2016 | A General Modular Synthesis Problem for Pushdown Systems. | Ilaria De Crescenzo, Salvatore La Torre |
| 2016 | Model Checking with Multi-threaded IC3 Portfolios. | Sagar Chaki, Derrick Karimi |
| 2016 | Automatic Generation of Propagation Complete SAT Encodings. | Martin Brain, Liana Hadarean, Daniel Kroening, Ruben Martins |
| 2016 | Predicate Abstraction for Linked Data Structures. | Alexander Bakst, Ranjit Jhala |
| 2016 | Tight Cutoffs for Guarded Protocols with Fairness. | Simon Auerlechner, Swen Jacobs, Ayrat Khalimov |
| 2016 | Viper: A Verification Infrastructure for Permission-Based Reasoning. | Peter Mller, Malte Schwerhoff, Alexander J. Summers |
| 2015 | Dependent Array Type Inference from Tests. | He Zhu, Aditya V. Nori, Suresh Jagannathan |
| 2015 | A Model for Industrial Real-Time Systems. | Md Tawhid Bin Waez, Andrzej Wasowski, Juergen Dingel, Karen Rudie |
| 2015 | Proving Guarantee and Recurrence Temporal Properties by Abstract Interpretation. | Caterina Urban, Antoine Min |
| 2015 | Debugging Process Algebra Specifications. | Gwen Salan, Lina Ye |
| 2015 | Distributed Markov Chains. | Ratul Saha, Javier Esparza, Sumit Kumar Jha, Madhavan Mukund, P. S. Thiagarajan |
| 2015 | Induction for SMT Solvers. | Andrew Reynolds, Viktor Kuncak |
| 2015 | Variations on the Stochastic Shortest Path Problem. | Mickael Randour, Jean-Franois Raskin, Ocan Sankur |
| 2015 | Foundations of Quantitative Predicate Abstraction for Stability Analysis of Hybrid Systems. | Pavithra Prabhakar, Miriam Garcia Soto |
| 2015 | Path Sensitive Cache Analysis Using Cache Miss Paths. | Kartik Nagar, Y. N. Srikant |
| 2015 | Bounded Implementations of Replicated Data Types. | Madhavan Mukund, Ranjal Gautham Shenoy, S. P. Suresh |
| 2015 | Abstraction of Arrays Based on Non Contiguous Partitions. | Jiangchao Liu, Xavier Rival |
| 2015 | Tree Automata-Based Refinement with Application to Horn Clause Verification. | Bishoksan Kafle, John P. Gallagher |