9. FMCAD 2010: Lugano, Switzerland

• Sumit Gulwani:
  Dimensions in program synthesis. 1
  
• Warren A. Hunt:
  Verifying VIA Nano microprocessor components. 3-10
  
• Joseph Sifakis:
  Embedded systems design - Scientific challenges and work directions. 11
  
• B. A. Krishna, Anamaya Sullerey, Alok Jain:
  Formal verification of an ASIC ethernet switch block. 13-20
  
• Gadiel Auerbach, Fady Copty, Viresh Paruthi:
  Formal verification of arbiters using property strengthening and underapproximations. 21-24
  
• Sabih Agbaria, Dan Carmi, Orly Cohen, Dmitry Korchemny, Michael Lifshits, Alexander Nadel:
  SAT-based semiformal verification of hardware. 25-32
  
• Lopamudra Sen, Amit Roy, Supriya Bhattacharjee, Bijitendra Mittra, Subir K. Roy:
  DFT logic verification through property based formal methods - SOC to IP. 33
  
• Thomas Ball, Ella Bounimova, Rahul Kumar, Vladimir Levin:
  SLAM2: Static driver verification with under 4% false alarms. 35-42
  
• Johannes Kinder, Helmut Veith:
  Precise static analysis of untrusted driver binaries. 43-50
  
• Alessandro Cimatti, Andrea Micheli, Iman Narasamdya, Marco Roveri:
  Verifying SystemC: A software model checking approach. 51-59
  
• Jason Baumgartner, Michael L. Case, Hari Mony:
  Coping with Moore's Law (and more): Supporting arrays in state-of-the-art model checkers. 61-69
  
• Pierluigi Nuzzo, Alberto Puggelli, Sanjit A. Seshia, Alberto L. Sangiovanni-Vincentelli:
  CalCS: SMT solving for non-linear convex constraints. 71-79
  
• Sicun Gao, Malay K. Ganai, Franjo Ivancic, Aarti Gupta, Sriram Sankaranarayanan, Edmund M. Clarke:
  Integrating ICP and LRA solvers for deciding nonlinear real arithmetic problems. 81-89
  
• ShengYu Shen, Ying Qin, Jianmin Zhang, Sikun Li:
  A halting algorithm to determine the existence of decoder. 91-99
  
• Jad Hamza, Barbara Jobstmann, Viktor Kuncak:
  Synthesis for regular specifications over unbounded domains. 101-109
  
• Michael Kuperstein, Martin T. Vechev, Eran Yahav:
  Automatic inference of memory fences. 111-119
  
• Anders Franzén, Alessandro Cimatti, Alexander Nadel, Roberto Sebastiani, Jonathan Shalev:
  Applying SMT in symbolic execution of microcode. 121-128
  
• Ulrich Kühne, Sven Beyer, Jörg Bormann, John Barstow:
  Automated formal verification of processors based on architectural models. 129-136
  
• Moshe Emmer, Zurab Khasidashvili, Konstantin Korovin, Andrei Voronkov:
  Encoding industrial hardware verification problems into effectively propositional logic. 137-144
  
• Hamid Savoj, David Berthelot, Alan Mishchenko, Robert K. Brayton:
  Combinational techniques for sequential equivalence checking. 145-149
  
• Jun Sawada:
  Automatic verification of estimate functions with polynomials of bounded functions. 151-158
  
• Peter Böhm:
  A framework for incremental modelling and verification of on-chip protocols. 159-166
  
• Eyad Alkassar, Ernie Cohen, Mark A. Hillebrand, Hristo Pentchev:
  Modular specification and verification of interprocess communication. 167-174
  
• Viresh Paruthi:
  Large-scale application of formal verification: From fiction to fact. 175-180
  
• Niklas Eén, Alan Mishchenko, Nina Amla:
  A single-instance incremental SAT formulation of proof- and counterexample-based abstraction. 181-188
  
• Dirk Beyer, M. Erkan Keremoglu, Philipp Wendler:
  Predicate abstraction with adjustable-block encoding. 189-197
  
• Nishant Sinha:
  Modular bug detection with inertial refinement. 199-206
  
• Joakim Urdahl, Dominik Stoffel, Jörg Bormann, Markus Wedler, Wolfgang Kunz:
  Path predicate abstraction by complete interval property checking. 207-215
  
• Leopold Haller, Satnam Singh:
  Relieving capacity limits on FPGA-based SAT-solvers. 217-220
  
• Alexander Nadel:
  Boosting minimal unsatisfiable core extraction. 221-229
  
• Malay K. Ganai:
  Propelling SAT and SAT-based BMC using careset. 231-238
  
• Christoph M. Wintersteiger, Youssef Hamadi, Leonardo Mendonça de Moura:
  Efficiently solving quantified bit-vector formulas. 239-246
  
• Alfons Laarman, Jaco van de Pol, Michael Weber:
  Boosting multi-core reachability performance with shared hash tables. 247-255
  
• Saddek Bensalem, Marius Bozga, Axel Legay, Thanh-Hung Nguyen, Joseph Sifakis, Rongjie Yan:
  Incremental component-based construction and verification using invariants. 257-256
  
• Eyad Alkassar, Ernie Cohen, Mark A. Hillebrand, Mikhail Kovalev, Wolfgang J. Paul:
  Verifying shadow page table algorithms. 267-270
  
• Massimo Roselli:
  Impacting verification closure using formal analysis. 271
  
• Gogul Balakrishnan, Malay K. Ganai, Aarti Gupta, Franjo Ivancic, Vineet Kahlon, Weihong Li, Naoto Maeda, Nadia Papakonstantinou, Sriram Sankaranarayanan, Nishant Sinha, Chao Wang:
  Scalable and precise program analysis at NEC. 273-274
  
• Michael Siegel:
  Achieving earlier verification closure using advanced formal verification. 275
  
• Hana Chockler:
  PINCETTE - Validating changes and upgrades in networked software. 277
  

Last update Fri May 25 08:14:14 2012 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page