Abstract is missing.
- How formal analysis and verification add security to blockchain-based systemsShin'ichiro Matsuo. 1-4 [doi]
- Symbolic security analysis using the Tamarin proverCas Cremers. 5 [doi]
- Coalition, intrigue, ambush, destruction and pride: Herding cats can be challengingJade Alglave. 6 [doi]
- Automated formal reasoning about AWS systemsByron Cook. 7 [doi]
- Formal methods in industrial dependable systems design - The TTTech exampleWilfried Steiner. 8 [doi]
- Hardware model checking competition 2017Armin Biere, Tom van Dijk, Keijo Heljanko. 9 [doi]
- The FMCAD 2017 graduate student forumKeijo Heljanko. 10 [doi]
- goSAT: Floating-point satisfiability as global optimizationM. Ammar Ben Khadra, Dominik Stoffel, Wolfgang Kunz. 11-14 [doi]
- On sound relative error bounds for floating-point arithmeticAnastasiia Izycheva, Eva Darulova. 15-22 [doi]
- Column-wise verification of multipliers using computer algebraDaniela Ritirc, Armin Biere, Manuel Kauers. 23-30 [doi]
- Efficient generation of all minimal inductive validity coresElaheh Ghassabani, Michael W. Whalen, Andrew Gacek. 31-38 [doi]
- Duality-based interpolation for quantifier-free equalities and uninterpreted functionsLeonardo Alt, Antti Eero Johannes Hyvärinen, Sepideh Asadi, Natasha Sharygina. 39-46 [doi]
- Solving linear arithmetic with SAT-based model checkingYakir Vizel, Alexander Nadel, Sharad Malik. 47-54 [doi]
- ZSstrS: A string solver with theory-aware heuristicsMurphy Berzish, Vijay Ganesh, Yunhui Zheng. 55-59 [doi]
- Verification of a lazy cache coherence protocol against a weak memory modelChristopher J. Banks, Marco Elver, Ruth Hoffmann, Susmit Sarkar, Paul Jackson, Vijay Nagarajan. 60-67 [doi]
- Safety verification of phaser programsZeinab Ganjei, Ahmed Rezine, Petru Eles, Zebo Peng. 68-75 [doi]
- Learning to prove safety over parameterised concurrent systemsYu-Fang Chen, Chih-Duo Hong, Anthony W. Lin, Philipp Rümmer. 76-83 [doi]
- Lasso detection using partial-state cachingRashmi Mudduluru, Pantazis Deligiannis, Ankush Desai, Akash Lal, Shaz Qadeer. 84-91 [doi]
- Exact quantitative probabilistic model checking through rational searchMatthew S. Bauer, Umang Mathur, Rohit Chadha, A. Prasad Sistla, Mahesh Viswanathan 0001. 92-99 [doi]
- Sampling invariants from frequency distributionsGrigory Fedyukovich, Samuel J. Kaufman, Rastislav Bodík. 100-107 [doi]
- Tagged BDDs: Combining reduction rules from different decision diagram typesTom van Dijk, Robert Wille, Robert Meolic. 108-115 [doi]
- First order temporal logic monitoring with BDDsKlaus Havelund, Doron Peled, Dogan Ulus. 116-123 [doi]
- Factored boolean functional synthesisLucas M. Tabajara, Moshe Y. Vardi. 124-131 [doi]
- Property directed reachability with word-level abstractionYen-Sheng Ho, Alan Mishchenko, Robert K. Brayton. 132-139 [doi]
- Learning support sets in IC3 and Quip: The good, the bad, and the uglyRyan Berryhill, Alexander Ivrii, Neil Veira, Andreas G. Veneris. 140-147 [doi]
- K-induction without unrollingArie Gurfinkel, Alexander Ivrii. 148-155 [doi]
- Designing parallel PDRMatteo Marescotti, Arie Gurfinkel, Antti Eero Johannes Hyvärinen, Natasha Sharygina. 156-163 [doi]
- FuseIC3: An algorithm for checking large design spacesRohit Dureja, Kristin Yvonne Rozier. 164-171 [doi]
- FAR-Cubicle - A new reachability algorithm for CubicleSylvain Conchon, Amit Goel, Sava Krstic, Rupak Majumdar, Mattias Roux. 172-175 [doi]
- Theta: A framework for abstraction refinement-based model checkingTamás Tóth, Ákos Hajdu, András Vörös, Zoltán Micskei, István Majzik. 176-179 [doi]
- Modular SMT-based analysis of nonlinear hybrid systemsKyungmin Bae, Sicun Gao. 180-187 [doi]
- SMT-based analysis of switching multi-domain linear Kirchhoff networksAlessandro Cimatti, Sergio Mover, Mirko Sessa. 188-195 [doi]
- Automatic verification of application-tailored OSEK kernelsHans-Peter Deifel, Merlin Gottlinger, Stefan Milius, Lutz Schröder, Christian Dietrich 0001, Daniel Lohmann. 196-203 [doi]
- Estimating worst-case latency of on-chip interconnects with formal simulationFreek Verbeek, Nike van Vugt. 204-211 [doi]
- Parameterized verification of algorithms for oblivious robots on a ringArnaud Sangnier, Nathalie Sznajder, Maria Potop-Butucaru, Sébastien Tixeuil. 212-219 [doi]
- Automated repair by example for firewallsWilliam T. Hallahan, Ennan Zhai, Ruzica Piskac. 220-229 [doi]