| 2014 | A Conference Management System with Verified Document Confidentiality. Sudeep Kanav, Peter Lammich, Andrei Popescu |
| 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 | 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 | A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors. Liana Hadarean, Kshitij Bansal, Dejan Jovanovic, Clark W. Barrett, Cesare Tinelli |
| 2014 | AVATAR: The Architecture for First-Order Theorem Provers. Andrei Voronkov |
| 2014 | An SMT-Based Approach to Coverability Analysis. Javier Esparza, Ruslán Ledesma-Garza, Rupak Majumdar, Philipp J. Meyer, Filip Niksic |
| 2014 | Analyzing and Synthesizing Genomic Logic Functions. Nicola Paoletti, Boyan Yordanov, Youssef Hamadi, Christoph M. Wintersteiger, Hillel Kugler |
| 2014 | Automatic Atomicity Verification for Clients of Concurrent Data Structures. Mohsen Lesani, Todd D. Millstein, Jens Palsberg |
| 2014 | Automating Separation Logic with Trees and Data. Ruzica Piskac, Thomas Wies, Damien Zufferey |
| 2014 | Bit-Vector Rewriting with Automatic Rule Generation. Alexander Nadel |
| 2014 | Bounded Model Checking of Multi-threaded C Programs via Lazy Sequentialization. Omar Inverso, Ermenegildo Tomasco, Bernd Fischer, Salvatore La Torre, Gennaro Parlato |
| 2014 | CEGAR for Qualitative Analysis of Probabilistic Systems. Krishnendu Chatterjee, Martin Chmelik, Przemyslaw Daca |
| 2014 | Causal Termination of Multi-threaded Programs. Andrey Kupriyanov, Bernd Finkbeiner |
| 2014 | Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings Armin Biere, Roderick Bloem |
| 2014 | Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR). Johannes Birgmeier, Aaron R. Bradley, Georg Weissenbacher |
| 2014 | Diamonds Are a Girl's Best Friend: Partial Order Reduction for Timed Automata with Abstractions. Henri Hansen, Shang-Wei Lin, Yang Liu, Truong Khanh Nguyen, Jun Sun |
| 2014 | Don't Sit on the Fence - A Static Analysis Approach to Automatic Fence Insertion. Jade Alglave, Daniel Kroening, Vincent Nimal, Daniel Poetzl |
| 2014 | Engineering a Static Verification Tool for GPU Kernels. Ethel Bardsley, Adam Betts, Nathan Chong, Peter Collingbourne, Pantazis Deligiannis, Alastair F. Donaldson, Jeroen Ketema, Daniel Liew, Shaz Qadeer |
| 2014 | Finding Instability in Biological Models. Byron Cook, Jasmin Fisher, Benjamin A. Hall, Samin Ishtiaq, Garvit Juniwal, Nir Piterman |
| 2014 | From Invariant Checking to Invariant Inference Using Randomized Search. Rahul Sharma, Alex Aiken |
| 2014 | From LTL to Deterministic Automata: A Safraless Compositional Approach. Javier Esparza, Jan Kretínský |
| 2014 | G4LTL-ST: Automatic Generation of PLC Programs. Chih-Hong Cheng, Chung-Hao Huang, Harald Ruess, Stefan Stattelmann |
| 2014 | GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components. Anton Wijs, Joost-Pieter Katoen, Dragan Bosnacki |
| 2014 | ICE: A Robust Framework for Learning Invariants. Pranav Garg, Christof Löding, P. Madhusudan, Daniel Neider |
| 2014 | Interpolating Property Directed Reachability. Yakir Vizel, Arie Gurfinkel |
| 2014 | Invariant Verification of Nonlinear Hybrid Automata Networks of Cardiac Cells. Zhenqi Huang, Chuchu Fan, Alexandru Mereacre, Sayan Mitra, Marta Z. Kwiatkowska |
| 2014 | LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes. Alejandro Sánchez, César Sánchez |
| 2014 | Lazy Annotation Revisited. Kenneth L. McMillan |
| 2014 | MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications. Petr Cermák, Alessio Lomuscio, Fabio Mogavero, Aniello Murano |
| 2014 | Minimizing Running Costs in Consumption Systems. Tomás Brázdil, David Klaska, Antonín Kucera, Petr Novotný |
| 2014 | Monadic Decomposition. Margus Veanes, Nikolaj S. Bjørner, Lev Nachmanson, Sergey Bereg |
| 2014 | Optimal Guard Synthesis for Memory Safety. Thomas Dillig, Isil Dillig, Swarat Chaudhuri |
| 2014 | Property-Directed Shape Analysis. Shachar Itzhaky, Nikolaj S. Bjørner, Thomas W. Reps, Mooly Sagiv, Aditya V. Thakur |
| 2014 | Proving Non-termination Using Max-SMT. Daniel Larraz, Kaustubh Nimkar, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio |
| 2014 | QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers. Arlen Cox, Bor-Yuh Evan Chang, Sriram Sankaranarayanan |
| 2014 | Reachability Analysis of Hybrid Systems Using Symbolic Orthogonal Projections. Willem Hagemann |
| 2014 | Regression Test Selection for Distributed Software Histories. Milos Gligoric, Rupak Majumdar, Rohan Sharma, Lamyaa Eloussi, Darko Marinov |
| 2014 | Regression-Free Synthesis for Concurrency. Pavol Cerný, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Thorsten Tarrach |
| 2014 | SMACK: Decoupling Source Language Details from Verifier Implementations. Zvonimir Rakamaric, Michael Emmi |
| 2014 | SMT-Based Model Checking for Recursive Programs. Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki |
| 2014 | Safraless Synthesis for Epistemic Temporal Specifications. Rodica Bozianu, Catalin Dima, Emmanuel Filiot |
| 2014 | Shape Analysis via Second-Order Bi-Abduction. Quang Loc Le, Cristian Gherghina, Shengchao Qin, Wei-Ngan Chin |
| 2014 | Software Verification in the Google App-Engine Cloud. Dirk Beyer, Georg Dresler, Philipp Wendler |
| 2014 | Solving Games without Controllable Predecessor. Nina Narodytska, Alexander Legg, Fahiem Bacchus, Leonid Ryzhyk, Adam Walker |
| 2014 | String Constraints for Verification. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukás Holík, Ahmed Rezine, Philipp Rümmer, Jari Stenman |
| 2014 | Symbolic Resource Bound Inference for Functional Programs. Ravichandhran Madhavan, Viktor Kuncak |
| 2014 | Symbolic Visibly Pushdown Automata. Loris D'Antoni, Rajeev Alur |
| 2014 | Synthesis of Masking Countermeasures against Side Channel Attacks. Hassan Eldib, Chao Wang |
| 2014 | Temporal Mode-Checking for Runtime Monitoring of Privacy Policies. Omar Chowdhury, Limin Jia, Deepak Garg, Anupam Datta |
| 2014 | Termination Analysis by Learning Terminating Programs. Matthias Heizmann, Jochen Hoenicke, Andreas Podelski |
| 2014 | The Spirit of Ghost Code. Jean-Christophe Filliâtre, Léon Gondelman, Andrei Paskevich |
| 2014 | The nuXmv Symbolic Model Checker. Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri, Stefano Tonetta |
| 2014 | Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction. Suho Lee, Karem A. Sakallah |
| 2014 | Vac - Verifier of Administrative Role-Based Access Control Policies. Anna Lisa Ferrara, P. Madhusudan, Truc L. Nguyen, Gennaro Parlato |
| 2014 | Verifying LTL Properties of Hybrid Systems with K-Liveness. Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta |
| 2014 | Verifying Relative Error Bounds Using Symbolic Simulation. Jesse Bingham, Joe Leslie-Hurd |
| 2014 | Yices 2.2. Bruno Dutertre |