default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID17th FMCAD 2017: Vienna, Austria
- Daryl Stewart, Georg Weissenbacher:
2017 Formal Methods in Computer Aided Design, FMCAD 2017, Vienna, Austria, October 2-6, 2017. IEEE 2017, ISBN 978-0-9835678-7-5
Invited Papers
- Shin'ichiro Matsuo:
How formal analysis and verification add security to blockchain-based systems. 1-4 - Cas Cremers:
Symbolic security analysis using the Tamarin prover. 5 - Jade Alglave:
Coalition, intrigue, ambush, destruction and pride: Herding cats can be challenging. 6 - Byron Cook:
Automated formal reasoning about AWS systems. 7 - Wilfried Steiner:
Formal methods in industrial dependable systems design - The TTTech example. 8 - Armin Biere
, Tom van Dijk, Keijo Heljanko:
Hardware model checking competition 2017. 9 - Keijo Heljanko:
The FMCAD 2017 graduate student forum. 10
Arithmetic
- M. Ammar Ben Khadra, Dominik Stoffel, Wolfgang Kunz:
goSAT: Floating-point satisfiability as global optimization. 11-14 - Anastasiia Izycheva, Eva Darulova:
On sound relative error bounds for floating-point arithmetic. 15-22 - Daniela Ritirc, Armin Biere, Manuel Kauers:
Column-wise verification of multipliers using computer algebra. 23-30
Solving
- Elaheh Ghassabani, Michael W. Whalen, Andrew Gacek:
Efficient generation of all minimal inductive validity cores. 31-38 - Leonardo Alt, Antti Eero Johannes Hyvärinen, Sepideh Asadi, Natasha Sharygina:
Duality-based interpolation for quantifier-free equalities and uninterpreted functions. 39-46 - Yakir Vizel, Alexander Nadel, Sharad Malik:
Solving linear arithmetic with SAT-based model checking. 47-54 - Murphy Berzish, Vijay Ganesh, Yunhui Zheng:
Z3str3: A string solver with theory-aware heuristics. 55-59
Concurrency and Distributed Systems
- Christopher J. Banks, Marco Elver, Ruth Hoffmann, Susmit Sarkar, Paul B. Jackson, Vijay Nagarajan:
Verification of a lazy cache coherence protocol against a weak memory model. 60-67 - Zeinab Ganjei, Ahmed Rezine, Petru Eles, Zebo Peng:
Safety verification of phaser programs. 68-75 - Yu-Fang Chen, Chih-Duo Hong, Anthony W. Lin, Philipp Rümmer:
Learning to prove safety over parameterised concurrent systems. 76-83 - Rashmi Mudduluru, Pantazis Deligiannis, Ankush Desai, Akash Lal, Shaz Qadeer:
Lasso detection using partial-state caching. 84-91
Probabilistic Systems
- Matthew S. Bauer, Umang Mathur, Rohit Chadha, A. Prasad Sistla, Mahesh Viswanathan:
Exact quantitative probabilistic model checking through rational search. 92-99 - Grigory Fedyukovich, Samuel J. Kaufman, Rastislav Bodík:
Sampling invariants from frequency distributions. 100-107
BDDs
- Tom van Dijk, Robert Wille, Robert Meolic:
Tagged BDDs: Combining reduction rules from different decision diagram types. 108-115 - Klaus Havelund, Doron Peled, Dogan Ulus:
First order temporal logic monitoring with BDDs. 116-123 - Lucas M. Tabajara, Moshe Y. Vardi:
Factored boolean functional synthesis. 124-131
IC3
- Yen-Sheng Ho, Alan Mishchenko, Robert K. Brayton:
Property directed reachability with word-level abstraction. 132-139 - Ryan Berryhill, Alexander Ivrii, Neil Veira, Andreas G. Veneris:
Learning support sets in IC3 and Quip: The good, the bad, and the ugly. 140-147 - Arie Gurfinkel, Alexander Ivrii:
K-induction without unrolling. 148-155 - Matteo Marescotti, Arie Gurfinkel, Antti Eero Johannes Hyvärinen, Natasha Sharygina:
Designing parallel PDR. 156-163 - Rohit Dureja, Kristin Yvonne Rozier:
FuseIC3: An algorithm for checking large design spaces. 164-171 - Sylvain Conchon, Amit Goel, Sava Krstic, Rupak Majumdar, Mattias Roux:
FAR-Cubicle - A new reachability algorithm for Cubicle. 172-175 - Tamás Tóth, Ákos Hajdu, András Vörös, Zoltán Micskei, István Majzik:
Theta: A framework for abstraction refinement-based model checking. 176-179
Hybrid Systems
- Kyungmin Bae, Sicun Gao:
Modular SMT-based analysis of nonlinear hybrid systems. 180-187 - Alessandro Cimatti, Sergio Mover, Mirko Sessa:
SMT-based analysis of switching multi-domain linear Kirchhoff networks. 188-195
Applications
- Hans-Peter Deifel, Merlin Göttlinger, Stefan Milius, Lutz Schröder, Christian Dietrich, Daniel Lohmann:
Automatic verification of application-tailored OSEK kernels. 196-203 - Freek Verbeek, Nike van Vugt:
Estimating worst-case latency of on-chip interconnects with formal simulation. 204-211 - Arnaud Sangnier, Nathalie Sznajder, Maria Potop-Butucaru, Sébastien Tixeuil:
Parameterized verification of algorithms for oblivious robots on a ring. 212-219 - William T. Hallahan, Ennan Zhai, Ruzica Piskac:
Automated repair by example for firewalls. 220-229
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2025-11-04 00:23 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
