Abstract is missing.
- PrefaceBarbara Jobstmann, Sandip Ray. [doi]
- Syntax-guided synthesisRajeev Alur, Rastislav Bodík, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, Abhishek Udupa. 1-17 [doi]
- Tutorial: Practical verification of network programsNate Foster, Arjun Guha, Mark Reitblatt, Cole Schlesinger. 9-10 [doi]
- Firmware validation: challenges and opportunitiesJim Grundy. 11 [doi]
- Secure programs via game-based synthesisSomesh Jha, Thomas W. Reps, William R. Harris. 12-13 [doi]
- Using process modeling and analysis techniques to reduce errors in healthcareLori A. Clarke. 14 [doi]
- Static verification based signoff - A key enabler for managing verification complexity in the modern socPranav Ashar. 15 [doi]
- The FMCAD graduate student forumThomas Wahl. 16-17 [doi]
- Distributed synthesis for LTL fragmentsKrishnendu Chatterjee, Thomas A. Henzinger, Jan Otop, Andreas Pavlogiannis. 18-25 [doi]
- Counter-strategy guided refinement of GR(1) temporal logic specificationsRajeev Alur, Salar Moarref, Ufuk Topcu. 26-33 [doi]
- Efficient handling of obligation constraints in synthesis from omega-regular specificationsSaqib Sohail, Fabio Somenzi. 34-41 [doi]
- On the feasibility of automation for bandwidth allocation problems in data centersYifei Yuan, Anduo Wang, Rajeev Alur, Boon Thau Loo. 42-45 [doi]
- Computing prime implicantsDavid Déharbe, Pascal Fontaine, Daniel Le Berre, Bertrand Mazure. 46-52 [doi]
- A circuit approach to LTL model checkingKoen Claessen, Niklas Eén, Baruch Sterin. 53-60 [doi]
- Invariants for finite instances and beyondSylvain Conchon, Amit Goel, Sava Krstic, Alain Mebsout, Fatiha Zaïdi. 61-68 [doi]
- Exploring interpolantsPhilipp Rümmer, Pavle Subotic. 69-76 [doi]
- Synthesizing multiple boolean functions using interpolation on a single proofGeorg Hofferek, Ashutosh Gupta, Bettina Könighofer, Jie-Hong Roland Jiang, Roderick Bloem. 77-84 [doi]
- Quantifier elimination via clause redundancyEugene Goldberg, Panagiotis Manolios. 85-92 [doi]
- Interpolation for synthesis on unbounded domainsViktor Kuncak, Régis Blanc. 93-96 [doi]
- Relational STE and theorem proving for formal verification of industrial circuit designsJohn W. O'Leary, Roope Kaivola, Tom Melham. 97-104 [doi]
- Satisfiability modulo ODEsSicun Gao, Soonho Kong, Edmund M. Clarke. 105-112 [doi]
- Verifying global convergence for a digital phase-locked loopJijie Wei, Yan Peng, Ge Yu, Mark R. Greenstreet. 113-120 [doi]
- Formal co-validation of low-level hardware/software interfacesAlex Horn, Michael Tautschnig, Celina G. Val, Lihao Liang, Tom Melham, Jim Grundy, Daniel Kroening. 121-128 [doi]
- An SMT based method for optimizing arithmetic computations in embedded software codeHassan Eldib, Chao Wang. 129-136 [doi]
- Verifying periodic programs with priority inheritance locksSagar Chaki, Arie Gurfinkel, Ofer Strichman. 137-144 [doi]
- Abstractions for model checking SDN controllersDivjyot Sethi, Srinivas Narayana, Sharad Malik. 145-148 [doi]
- Efficient modular SAT solving for IC3Sam Bayless, Celina G. Val, Thomas Ball, Holger H. Hoos, Alan J. Hu. 149-156 [doi]
- Better generalization in IC3Zyad Hassan, Aaron R. Bradley, Fabio Somenzi. 157-164 [doi]
- Parameter synthesis with IC3Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta. 165-168 [doi]
- Generalized counterexamples to liveness propertiesGadi Aleksandrowicz, Jason Baumgartner, Alexander Ivrii, Ziv Nevo. 169-180 [doi]
- Trimming while checking clausal proofsMarijn Heule, Warren A. Hunt Jr., Nathan Wetzler. 181-188 [doi]
- Simplex with sum of infeasibilities for SMTTim King, Clark Barrett, Bruno Dutertre. 189-196 [doi]
- Efficient MUS extraction with resolutionAlexander Nadel, Vadim Ryvchin, Ofer Strichman. 197-200 [doi]
- Parameterized model checking of fault-tolerant distributed algorithms by abstractionAnnu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder. 201-209 [doi]
- Verifying multi-threaded software with impactBjörn Wachter, Daniel Kroening, Joël Ouaknine. 210-217 [doi]
- Proving termination of imperative programs using Max-SMTDaniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio. 218-225 [doi]
- On the concept of variable roles and its use in software analysisYulia Demyanova, Helmut Veith, Florian Zuleger. 226-230 [doi]