| 2014 | AVATAR: The Architecture for First-Order Theorem Provers. | Andrei Voronkov |
| 2014 | Interpolating Property Directed Reachability. | Yakir Vizel, Arie Gurfinkel |
| 2014 | Monadic Decomposition. | Margus Veanes, Nikolaj S. Bjrner, Lev Nachmanson, Sergey Bereg |
| 2014 | A Nonlinear Real Arithmetic Fragment. | Ashish Tiwari, Patrick Lincoln |
| 2014 | A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis. | Moritz Sinn, Florian Zuleger, Helmut Veith |
| 2014 | Formal Replay of Translation Validation for Highly Optimised C. | Thomas Sewell |
| 2014 | LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes. | Alejandro Snchez, Csar Snchez |
| 2014 | SMACK: Decoupling Source Language Details from Verifier Implementations. | Zvonimir Rakamaric, Michael Emmi |
| 2014 | Automating Separation Logic with Trees and Data. | Ruzica Piskac, Thomas Wies, Damien Zufferey |
| 2014 | Analyzing and Synthesizing Genomic Logic Functions. | Nicola Paoletti, Boyan Yordanov, Youssef Hamadi, Christoph M. Wintersteiger, Hillel Kugler |
| 2014 | Verification of Multi-Party Ping-Pong Protocols via Program Transformation. | Antonina Nepeivoda |
| 2014 | On Unfolding for Programs Using Strings as a Data Type. | Andrei P. Nemytykh |
| 2014 | Solving Games without Controllable Predecessor. | Nina Narodytska, Alexander Legg, Fahiem Bacchus, Leonid Ryzhyk, Adam Walker |
| 2014 | Bit-Vector Rewriting with Automatic Rule Generation. | Alexander Nadel |
| 2014 | Lazy Annotation Revisited. | Kenneth L. McMillan |
| 2014 | Symbolic Resource Bound Inference for Functional Programs. | Ravichandhran Madhavan, Viktor Kuncak |
| 2014 | A Note on Program Specialization. What Syntactical Properties of Residual Programs Can Reveal? | Alexei Lisitsa, Andrei P. Nemytykh |
| 2014 | A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions. | Tianyi Liang, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett, Morgan Deters |
| 2014 | Towards Constraint-Solving over Higher-Order Unbounded Datatypes using Formal Methods Tools. | Michael Leuschel |
| 2014 | Automatic Atomicity Verification for Clients of Concurrent Data Structures. | Mohsen Lesani, Todd D. Millstein, Jens Palsberg |
| 2014 | Shape Analysis via Second-Order Bi-Abduction. | Quang Loc Le, Cristian Gherghina, Shengchao Qin, Wei-Ngan Chin |
| 2014 | Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction. | Suho Lee, Karem A. Sakallah |
| 2014 | Proving Non-termination Using Max-SMT. | Daniel Larraz, Kaustubh Nimkar, Albert Oliveras, Enric Rodrguez-Carbonell, Albert Rubio |
| 2014 | Causal Termination of Multi-threaded Programs. | Andrey Kupriyanov, Bernd Finkbeiner |
| 2014 | SMT-Based Model Checking for Recursive Programs. | Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki |