| 2013 | A circuit approach to LTL model checking. Koen Claessen, Niklas Eén, Baruch Sterin |
| 2013 | Abstractions for model checking SDN controllers. Divjyot Sethi, Srinivas Narayana, Sharad Malik |
| 2013 | An SMT based method for optimizing arithmetic computations in embedded software code. Hassan Eldib, Chao Wang |
| 2013 | Better generalization in IC3. Zyad Hassan, Aaron R. Bradley, Fabio Somenzi |
| 2013 | Computing prime implicants. David Déharbe, Pascal Fontaine, Daniel Le Berre, Bertrand Mazure |
| 2013 | Counter-strategy guided refinement of GR(1) temporal logic specifications. Rajeev Alur, Salar Moarref, Ufuk Topcu |
| 2013 | Distributed synthesis for LTL fragments. Krishnendu Chatterjee, Thomas A. Henzinger, Jan Otop, Andreas Pavlogiannis |
| 2013 | Efficient MUS extraction with resolution. Alexander Nadel, Vadim Ryvchin, Ofer Strichman |
| 2013 | Efficient handling of obligation constraints in synthesis from omega-regular specifications. Saqib Sohail, Fabio Somenzi |
| 2013 | Efficient modular SAT solving for IC3. Sam Bayless, Celina G. Val, Thomas Ball, Holger H. Hoos, Alan J. Hu |
| 2013 | Exploring interpolants. Philipp Rümmer, Pavle Subotic |
| 2013 | Firmware validation: challenges and opportunities. Jim Grundy |
| 2013 | Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013 |
| 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 | Generalized counterexamples to liveness properties. Gadi Aleksandrowicz, Jason Baumgartner, Alexander Ivrii, Ziv Nevo |
| 2013 | Interpolation for synthesis on unbounded domains. Viktor Kuncak, Régis Blanc |
| 2013 | Invariants for finite instances and beyond. Sylvain Conchon, Amit Goel, Sava Krstic, Alain Mebsout, Fatiha Zaïdi |
| 2013 | On the concept of variable roles and its use in software analysis. Yulia Demyanova, Helmut Veith, Florian Zuleger |
| 2013 | On the feasibility of automation for bandwidth allocation problems in data centers. Yifei Yuan, Anduo Wang, Rajeev Alur, Boon Thau Loo |
| 2013 | Parameter synthesis with IC3. Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta |
| 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 | Proving termination of imperative programs using Max-SMT. Daniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio |
| 2013 | Quantifier elimination via clause redundancy. Eugene Goldberg, Panagiotis Manolios |
| 2013 | Relational STE and theorem proving for formal verification of industrial circuit designs. John W. O'Leary, Roope Kaivola, Tom Melham |
| 2013 | Satisfiability modulo ODEs. Sicun Gao, Soonho Kong, Edmund M. Clarke |
| 2013 | Secure programs via game-based synthesis. Somesh Jha, Thomas W. Reps, William R. Harris |
| 2013 | Simplex with sum of infeasibilities for SMT. Tim King, Clark W. Barrett, Bruno Dutertre |
| 2013 | Static verification based signoff - A key enabler for managing verification complexity in the modern soc. Pranav Ashar |
| 2013 | Syntax-guided synthesis. Rajeev Alur, Rastislav Bodík, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, Abhishek Udupa |
| 2013 | Synthesizing multiple boolean functions using interpolation on a single proof. Georg Hofferek, Ashutosh Gupta, Bettina Könighofer, Jie-Hong Roland Jiang, Roderick Bloem |
| 2013 | The FMCAD graduate student forum. Thomas Wahl |
| 2013 | Trimming while checking clausal proofs. Marijn Heule, Warren A. Hunt Jr., Nathan Wetzler |
| 2013 | Tutorial: Practical verification of network programs. Nate Foster, Arjun Guha, Mark Reitblatt, Cole Schlesinger |
| 2013 | Using process modeling and analysis techniques to reduce errors in healthcare. Lori A. Clarke |
| 2013 | Verifying global convergence for a digital phase-locked loop. Jijie Wei, Yan Peng, Ge Yu, Mark R. Greenstreet |
| 2013 | Verifying multi-threaded software with impact. Björn Wachter, Daniel Kroening, Joël Ouaknine |
| 2013 | Verifying periodic programs with priority inheritance locks. Sagar Chaki, Arie Gurfinkel, Ofer Strichman |