| 2015 | Effective Search-Space Pruning for Solvers of String Equations, Regular Expressions and Length Constraints. | Yunhui Zheng, Vijay Ganesh, Sanu Subramanian, Omer Tripp, Julian Dolby, Xiangyu Zhang |
| 2015 | Fast Interpolating BMC. | Yakir Vizel, Arie Gurfinkel, Sharad Malik |
| 2015 | Modular Deductive Verification of Multiprocessor Hardware Designs. | Muralidaran Vijayaraghavan, Adam Chlipala, Arvind, Nirav Dave |
| 2015 | Time-Aware Abstractions in HybridSal. | Ashish Tiwari |
| 2015 | Predicting a Correct Program in Programming by Example. | Rishabh Singh, Sumit Gulwani |
| 2015 | ProbReach: A Tool for Guaranteed Reachability Analysis of Stochastic Hybrid Systems. | Fedor Shmarov, Paolo Zuliani |
| 2015 | OptiMathSAT: A Tool for Optimization Modulo Theories. | Roberto Sebastiani, Patrick Trentin |
| 2015 | Symbolic-Numeric Reachability Analysis of Hybrid Systems. | Sriram Sankaranarayanan |
| 2015 | Alchemist: Learning Guarded Affine Functions. | Shambwaditya Saha, Pranav Garg, P. Madhusudan |
| 2015 | Counterexample-Guided Quantifier Instantiation for Synthesis in SMT. | Andrew Reynolds, Morgan Deters, Viktor Kuncak, Cesare Tinelli, Clark W. Barrett |
| 2015 | A Type-Directed Approach to Program Repair. | Alex Reinking, Ruzica Piskac |
| 2015 | Percentile Queries in Multi-dimensional Markov Decision Processes. | Mickael Randour, Jean-Franois Raskin, Ocan Sankur |
| 2015 | An Algorithmic Approach to Stability Verification of Hybrid Systems: A Summary. | Pavithra Prabhakar, Miriam Garcia Soto |
| 2015 | Systematic Asynchrony Bug Exploration for Android Apps. | Burcu Kulahcioglu Ozkan, Michael Emmi, Serdar Tasiran |
| 2015 | Abstract Interpretation with Higher-Dimensional Ellipsoids and Conic Extrapolation. | Mendes Oulamara, Arnaud J. Venet |
| 2015 | A Summary of Recent Progress on Efficient Parametric Approximations of Viability and Discriminating Kernels. | Ian Mitchell |
| 2015 | PVSio-web 2.0: Joining PVS to HCI. | Paolo Masci, Patrick Oladimeji, Yi Zhang, Paul L. Jones, Paul Curzon, Harold W. Thimbleby |
| 2015 | An Axiomatic Specification for Sequential Memory Models. | William Mansky, Dmitri Garbuzov, Steve Zdancewic |
| 2015 | The Inez Mathematical Programming Modulo Theories Framework. | Panagiotis Manolios, Jorge Pais, Vasilis Papavasileiou |
| 2015 | Bbs: A Phase-Bounded Model Checker for Asynchronous Programs. | Rupak Majumdar, Zilong Wang |
| 2015 | Verifying Linearizability of Intel Software Guard Extensions. | Rebekah Leslie-Hurd, Dror Caspi, Matthew Fernandez |
| 2015 | Fine-Grained Caching of Verification Results. | K. Rustan M. Leino, Valentin Wstholz |
| 2015 | Automatic Rootcausing for Program Equivalence Failures in Binaries. | Shuvendu K. Lahiri, Rohit Sinha, Chris Hawblitzel |
| 2015 | Predicate Abstraction and CEGAR for Disproving Termination of Higher-Order Functional Programs. | Takuya Kuwahara, Ryosuke Sato, Hiroshi Unno, Naoki Kobayashi |
| 2015 | SMT and POR Beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms. | Igor Konnov, Helmut Veith, Josef Widder |