| 2013 | Abstractions for model checking SDN controllers. | Divjyot Sethi, Srinivas Narayana, Sharad Malik |
| 2013 | Exploring interpolants. | Philipp Rmmer, Pavle Subotic |
| 2013 | Lemmas on Demand for Lambdas. | Mathias Preiner, Aina Niemetz, Armin Biere |
| 2013 | Trading-off Incrementality and Dynamic Restart of Multiple Solvers in IC3. | Marco Palena, Gianpiero Cabodi, Alan Mishchenko |
| 2013 | Relational STE and theorem proving for formal verification of industrial circuit designs. | John W. O'Leary, Roope Kaivola, Tom Melham |
| 2013 | Efficient MUS extraction with resolution. | Alexander Nadel, Vadim Ryvchin, Ofer Strichman |
| 2013 | Abstraction-Based Livelock/Deadlock Checking for Hardware Verification. | In-Ho Moon, Kevin Harer |
| 2013 | LEC: Learning Driven Data-path Equivalence Checking. | Jiang Long, Robert K. Brayton, Michael L. Case |
| 2013 | Proving termination of imperative programs using Max-SMT. | Daniel Larraz, Albert Oliveras, Enric Rodrguez-Carbonell, Albert Rubio |
| 2013 | Interpolation for synthesis on unbounded domains. | Viktor Kuncak, Rgis Blanc |
| 2013 | Simplex with sum of infeasibilities for SMT. | Tim King, Clark W. Barrett, Bruno Dutertre |
| 2013 | Parameterized model checking of fault-tolerant distributed algorithms by abstraction. | Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder |
| 2013 | Preface. | Barbara Jobstmann, Sandip Ray |
| 2013 | Secure programs via game-based synthesis. | Somesh Jha, Thomas W. Reps, William R. Harris |
| 2013 | Formal co-validation of low-level hardware/software interfaces. | Alex Horn, Michael Tautschnig, Celina G. Val, Lihao Liang, Tom Melham, Jim Grundy, Daniel Kroening |
| 2013 | Synthesizing multiple boolean functions using interpolation on a single proof. | Georg Hofferek, Ashutosh Gupta, Bettina Knighofer, Jie-Hong Roland Jiang, Roderick Bloem |
| 2013 | Trimming while checking clausal proofs. | Marijn Heule, Warren A. Hunt Jr., Nathan Wetzler |
| 2013 | Better generalization in IC3. | Zyad Hassan, Aaron R. Bradley, Fabio Somenzi |
| 2013 | Firmware validation: challenges and opportunities. | Jim Grundy |
| 2013 | Quantifier elimination via clause redundancy. | Eugene Goldberg, Panagiotis Manolios |
| 2013 | Satisfiability modulo ODEs. | Sicun Gao, Soonho Kong, Edmund M. Clarke |
| 2013 | Tutorial: Practical verification of network programs. | Nate Foster, Arjun Guha, Mark Reitblatt, Cole Schlesinger |
| 2013 | An SMT based method for optimizing arithmetic computations in embedded software code. | Hassan Eldib, Chao Wang |
| 2013 | A Fast Reparameterization Procedure. | Niklas En, Alan Mishchenko |
| 2013 | CHIMP: A Tool for Assertion-Based Dynamic Verification of SystemC Models. | Sonali Dutta, Moshe Y. Vardi, Deian Tabakov |