Abstract is missing.
- Formal verification for computer security: Lessons learned and future directionsDawn Song. 1 [doi]
- Understanding evolution through algorithmsChristos Papadimitriou. 2 [doi]
- Network verification - When Clarke meets CerfGeorge Varghese. 3 [doi]
- Machine learning and systems for the next frontier in formal verificationManish Pandey. 4 [doi]
- Verifying hyperproperties of hardware systemsBernd Finkbeiner, Markus N. Rabe. 5 [doi]
- A paradigm shift in verification methodologyPranav Ashar. 6 [doi]
- Program synthesis for networksPavol Cerný. 7 [doi]
- The FMCAD 2016 graduate student forumHossein Hojjat. 8 [doi]
- Soundness of the quasi-synchronous abstractionGuillaume Baudart, Timothy Bourke, Marc Pouzet. 9-16 [doi]
- Synthesizing adaptive test strategies from temporal logic specificationsRoderick Bloem, Robert Könighofer, Ingo Pill, Franz Röck. 17-24 [doi]
- Reducing interpolant circuit size by ad-hoc logic synthesis and SAT-based weakeningGianpiero Cabodi, Paolo Camurati, Marco Palena, P. Pasini, Danilo Vendraminetto. 25-32 [doi]
- Extracting behaviour from an executable instruction set modelBrian Campbell 0001, Ian Stark. 33-40 [doi]
- Categorical semantics of digital circuitsDan R. Ghica, Achim Jung. 41-48 [doi]
- Equivalence checking by logic relaxationEugene Goldberg. 49-56 [doi]
- Minimal unsatisfiable core extraction for SMTOfer Guthmann, Ofer Strichman, Anna Trostanetski. 57-64 [doi]
- Efficient uninterpreted function abstraction and refinement for word-level model checkingYen-Sheng Ho, Pankaj Chauhan, Pritam Roy, Alan Mishchenko, Robert K. Brayton. 65-72 [doi]
- Optimizing horn solvers for network repairHossein Hojjat, Philipp Rümmer, Jedidiah McClurg, Pavol Cerný, Nate Foster. 73-80 [doi]
- On ∃ ∀ ∃! solving: A case study on automated synthesis of magic card tricksSusmit Jha, Vasumathi Raman, Sanjit A. Seshia. 81-84 [doi]
- Property-directed k-inductionDejan Jovanovic, Bruno Dutertre. 85-92 [doi]
- Lazy proofs for DPLL(T)-based SMT solversGuy Katz, Clark W. Barrett, Cesare Tinelli, Andrew Reynolds, Liana Hadarean. 93-100 [doi]
- Verifiable hierarchical protocols with network invariants on parametric systemsOpeoluwa Matthews, Jesse D. Bingham, Daniel J. Sorin. 101-108 [doi]
- Modular specification and verification of a cache-coherent interfaceKenneth L. McMillan. 109-116 [doi]
- Proof certificates for SMT-based model checkers for infinite-state systemsAlain Mebsout, Cesare Tinelli. 117-124 [doi]
- Routing under constraintsAlexander Nadel. 125-132 [doi]
- A consistency checker for memory subsystem tracesMatthew Naylor, Simon W. Moore, Alan Mujumdar. 133-140 [doi]
- Hybrid partial order reduction with under-approximate dynamic points-to and determinacy informationPavel Parizek. 141-148 [doi]
- Formal verification of division and square root implementations, an Oracle reportDavid L. Rager, Jo C. Ebergen, Dmitry Nadezhin, Austin Lee, Cuong Kim Chau, Ben Selfridge. 149-152 [doi]
- Integrating proxy theories and numeric model lifting for floating-point arithmeticJaideep Ramachandran, Thomas Wahl. 153-160 [doi]
- Trustworthy specifications of ARM® v8-A and v8-M system level architectureAlastair Reid. 161-168 [doi]
- Equivalence checking using Gröbner basesAmr A. R. Sayed-Ahmed, Daniel Große, Mathias Soeken, Rolf Drechsler. 169-176 [doi]
- Accurate ICP-based floating-point reasoningKarsten Scheibler, Felix Neubauer, Ahmed Mahdi, Martin Fränzle, Tino Teige, Tom Bienmüller, Detlef Fehrer, Bernd Becker 0001. 177-184 [doi]
- SWAPPER: A framework for automatic generation of formula simplifiers based on conditional rewrite rulesRohit Singh 0002, Armando Solar-Lezama. 185-192 [doi]
- Lazy sequentialization for TSO and PSO via shared memory abstractionsErmenegildo Tomasco, Truc L. Nguyen, Omar Inverso, Bernd Fischer 0002, Salvatore La Torre, Gennaro Parlato. 193-200 [doi]
- Combining requirement mining, software model checking and simulation-based verification for industrial automotive systemsTomoya Yamaguchi, Tomoyuki Kaga, Alexandre Donzé, Sanjit A. Seshia. 201-204 [doi]