Abstract is missing.
- Challenging problems in industrial formal verificationZiyad Hanna. 1 [doi]
- Challenges in bit-precise reasoningArmin Biere. 3 [doi]
- Efficient symbolic execution for software testingJohannes Kinder. 5 [doi]
- A tour of CVC4: How it works, and how to use itMorgan Deters, Andrew Reynolds, Tim King 0001, Clark W. Barrett, Cesare Tinelli. 7 [doi]
- Compiler verification for fun and profitXavier Leroy. 9 [doi]
- Computer-aided verification technology for biologyThomas A. Henzinger. 11 [doi]
- The FMCAD 2014 graduate student forumRuzica Piskac. 13 [doi]
- Response property checking via distributed state space explorationBrad D. Bingham, Mark R. Greenstreet. 15-22 [doi]
- Towards Pareto-optimal parameter synthesis for monotonie cost functionsBenjamin Bittner, Marco Bozzano, Alessandro Cimatti, Marco Gario, Alberto Griggio. 23-30 [doi]
- SAT-based methods for circuit synthesisRoderick Bloem, Uwe Egly, Patrick Klampfl, Robert Könighofer, Florian Lonsing. 31-34 [doi]
- Synthesis of synchronization using uninterpreted functionsRoderick Bloem, Georg Hofferek, Bettina Könighofer, Robert Könighofer, Simon Ausserlechner, Raphael Spork. 35-42 [doi]
- Interpolation with Guided Refinement: Revisiting incrementality in SAT-based unbounded model checkingGianpiero Cabodi, Marco Palena, P. Pasini. 43-50 [doi]
- Efficient verification of periodic programs using sequential consistency and snapshotsSagar Chaki, Arie Gurfinkel, Nishant Sinha. 51-58 [doi]
- Under-approximate flowpipes for non-linear continuous systemsXin Chen Rwth, Sriram Sankaranarayanan, Erika Ábrahám. 59-66 [doi]
- Disproving termination with overapproximationByron Cook, Carsten Fuhs, Kaustubh Nimkar, Peter W. O'Hearn. 67-74 [doi]
- Faster temporal reasoning for infinite-state programsByron Cook, Heidy Khlaaf, Nir Piterman. 75-82 [doi]
- Template-based circuit understandingAdria Gascón, Pramod Subramanyan, Bruno Dutertre, Ashish Tiwari, Dejan Jovanovic, Sharad Malik. 83-90 [doi]
- Simulation and formal verification of x86 machine-code programs that make system callsShilpi Goel, Warren A. Hunt Jr., Matt Kaufmann, Soumava Ghosh. 91-98 [doi]
- DRUPing for interpolatesArie Gurfinkel, Yakir Vizel. 99-106 [doi]
- Efficient extraction of Skolem functions from QRAT proofsMarijn Heule, Martina Seidl, Armin Biere. 107-114 [doi]
- Small inductive safe invariantsAlexander Ivrii, Arie Gurfinkel, Anton Belov. 115-122 [doi]
- On interpolants and variable assignmentsPavel Jancík, Jan Kofron, Simone Fulvio Rollini, Natasha Sharygina. 123-130 [doi]
- Post-silicon timing diagnosis made simple using formal technologyDaher Kaiss, Jonathan Kalechstain. 131-138 [doi]
- Leveraging linear and mixed integer programming for SMTTim King 0001, Clark W. Barrett, Cesare Tinelli. 139-146 [doi]
- A program transformation for faster goal-directed searchAkash Lal, Shaz Qadeer. 147-154 [doi]
- Infinite-state backward exploration of Boolean broadcast programsPeizun Liu, Thomas Wahl. 155-162 [doi]
- Kuai: A model checker for software-defined networksRupak Majumdar, Sai Deep Tetali, Zilong Wang. 163-170 [doi]
- ILP Modulo DataPanagiotis Manolios, Vasilis Papavasileiou, Mirek Riedewald. 171-178 [doi]
- Turbo-charging Lemmas on demand with don't care reasoningAina Niemetz, Mathias Preiner, Armin Biere. 179-186 [doi]
- Reduction for compositional verification of multi-threaded programsCorneliu Popeea, Andrey Rybalchenko, Andreas Wilhelm. 187-194 [doi]
- Finding conflicting instances of quantified formulas in SMTAndrew Reynolds, Cesare Tinelli, Leonardo Mendonça de Moura. 195-202 [doi]
- Using interval constraint propagation for pseudo-Boolean constraint solvingKarsten Scheibler, Bernd Becker. 203-206 [doi]
- Patient-specific models from inter-patient biological models and clinical recordsEnrico Tronci, Toni Mancini, Ivano Salvo, Stefano Sinisi, Federico Mari, Igor Melatti, Annalisa Massini, Francesco Davi, Thomas Dierkes, Rainald Ehrig, Susanna Röblitz, Brigitte Leeners, Tillmann H. C. Kruger, Marcel Egli, Fabian Ille. 207-214 [doi]
- Reducing CTL-live model checking to first-order logic validity checkingAmirhossein Vakili, Nancy A. Day. 215-218 [doi]
- Predicate abstraction for reactive synthesisAdam Walker, Leonid Ryzhyk. 219-226 [doi]