8. FMCAD 2009: Austin, Texas, USA

Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2009, 15-18 November 2009, Austin, Texas, USA. IEEE 2009, ISBN 978-1-4244-4966-8

Model Checking

Yakir Vizel, Orna Grumberg:
Interpolation-sequence based model checking. 1-8
Alessandro Cimatti, Jori Dubrovin, Tommi A. Junttila, Marco Roveri:
Structure-aware computation of predicate abstraction. 9-16
Michael L. Case, Hari Mony, Jason Baumgartner, Robert Kanzelman:
Enhanced verification by temporal decomposition. 17-24

Software Verification

Dirk Beyer, Alessandro Cimatti, Alberto Griggio, M. Erkan Keremoglu, Roberto Sebastiani:
Software model checking via large-block encoding. 25-32
Jyotirmoy V. Deshmukh, E. Allen Emerson:
Verification of recursive methods on tree-like data structures. 33-40
Subodh Sharma, Ganesh Gopalakrishnan, Eric Mercer, Jim Holt:
MCC: A runtime verification tool for MCAPI user applications. 41-44

Satisfiability Modulo Theory

Leonardo Mendonça de Moura, Nikolaj Bjørner:
Generalized, efficient array decision procedures. 45-52
Sagar Chaki, Arie Gurfinkel, Ofer Strichman:
Decision diagrams for linear arithmetic. 53-60
Malay K. Ganai, Franjo Ivancic:
Efficient decision procedure for non-linear arithmetic constraints using CORDIC. 61-68
Angelo Brillout, Daniel Kroening, Thomas Wahl:
Mixed abstractions for floating-point arithmetic. 69-76

Games

Saqib Sohail, Fabio Somenzi:
Safety first: A two-stage algorithm for LTL games. 77-84
Roderick Bloem, Karin Greimel, Thomas A. Henzinger, Barbara Jobstmann:
Synthesizing robust systems. 85-92

Quantitative Reasoning

William Denman, Behzad Akbarpour, Sofiène Tahar, Mohamed H. Zaki, Lawrence C. Paulson:
Formal verification of analog designs using MetiTarski. 93-100
Krishnan Kailas, Viresh Paruthi, Brian Monwai:
Formal verification of correctness and performance of random priority-based arbiters. 101-107

Assume Guarantee Reasoning

Zurab Khasidashvili, Gavriel Gavrielov, Tom Melham:
Assume-guarantee validation for STE properties within an SVA environment. 108-115
He Zhu, Fei He, William N. N. Hung, Xiaoyu Song, Ming Gu:
Data mining based decomposition for assume-guarantee reasoning. 116-119

Equivalence Checking

Jason Baumgartner, Hari Mony, Michael L. Case, Jun Sawada, Karen Yorav:
Scalable conditional equivalence checking: An automated invariant-generation based approach. 120-127
Zurab Khasidashvili, Mahmoud Kinanah, Andrei Voronkov:
Verifying equivalence of memories using a first order logic theorem prover. 128-135
Zurab Khasidashvili, Daher Kaiss, Doron Bustan:
A compositional theory for post-reboot observational equivalence checking of hardware. 136-143

Debugging

Brian Keng, Andreas G. Veneris:
Scaling VLSI design debugging with interpolation. 144-151
Robert Könighofer, Georg Hofferek, Roderick Bloem:
Debugging formal specifications using simple counterstrategies. 152-159
Sandip Ray, Warren A. Hunt Jr.:
Connecting pre-silicon and post-silicon verification. 160-163

Case Studies and Verification in the Large

Sergey Tverdyshev:
A verified platform for a gate-level electronic control unit. 164-171
John W. O'Leary, Murali Talupur, Mark R. Tuttle:
Protocol verification using flows: An industrial experience. 172-179
Jesse D. Bingham, John Erickson, Gaurav Singh, Flemming Andersen:
Industrial strength refinement checking. 180-183
Tom van den Broek, Julien Schmaltz:
Towards a formally verified network-on-chip. 184-187
Levent Erkök, Magnus Carlsson, Adam Wick:
Hardware/software co-verification of cryptographic algorithms using Cryptol. 188-191

Synthesis

Hai Zhou:
Retiming and resynthesis with sweep are complete for sequential transformation. 192-197
Eli Arbel, Oleg Rokhlenko, Karen Yorav:
SAT-based synthesis of clock gating functions using 3-valued abstraction. 198-204
Byron Cook, Ashutosh Gupta, Stephen Magill, Andrey Rybalchenko, Jirí Simsa, Satnam Singh, Viktor Vafeiadis:
Finding heap-bounds for hardware synthesis. 205-212

Last update Sat May 25 02:54:01 2013 CET by the DBLP Team —

Data released under the ODC-BY 1.0 license — See also our legal information page