7. FMCAD 2007: Austin, Texas, USA

SAT-Based Methods

• Jocelyn Simmonds, Jessica Davies, Arie Gurfinkel, Marsha Chechik:
  Exploiting Resolution Proofs to Speed Up LTL Vacuity Detection for BMC. 3-12
  
• Sean Safarpour, Hratch Mangassarian, Andreas G. Veneris, Mark H. Liffiton, Karem A. Sakallah:
  Improved Design Debugging Using Maximum Satisfiability. 13-19
  
• Daher Kaiss, Marcelo Skaba, Ziyad Hanna, Zurab Khasidashvili:
  Industrial Strength SAT-based Alignability Algorithm for Hardware Equivalence Verification. 20-26
  
• Frank Hutter, Domagoj Babic, Holger H. Hoos, Alan J. Hu:
  Boosting Verification by Automatic Tuning of Decision Procedures. 27-34
  

High-Level System Analysis

• Ariel Cohen, John W. O'Leary, Amir Pnueli, Mark R. Tuttle, Lenore D. Zuck:
  Verifying Correctness of Transactional Memories. 37-44
  
• Naghmeh Ghafari, Arie Gurfinkel, Nils Klarlund, Richard J. Trefler:
  Algorithmic Analysis of Piecewise FIFO Systems. 45-52
  
• Xiaofang Chen, Steven M. German, Ganesh Gopalakrishnan:
  Transaction Based Modeling and Verification of Hardware Protocols. 53-61
  
• Yogesh S. Mahajan, Sharad Malik:
  Automating Hazard Checking in Transaction-Level Microarchitecture Models. 62-65
  

Abstraction-Based Methods

• Roberto Cavada, Alessandro Cimatti, Anders Franzén, Krishnamani Kalyanasundaram, Marco Roveri, R. K. Shyamasundar:
  Computing Predicate Abstractions by Integrating BDDs and SMT Solvers. 69-76
  
• Chao Wang, Aarti Gupta, Franjo Ivancic:
  Induction in CEGAR for Detecting Counterexamples. 77-84
  
• Daniel Kroening, Georg Weissenbacher:
  Lifting Propositional Interpolants to the Word-Level. 85-89
  

Software Analysis Methods

• Fadi A. Zaraket, John Pape, Adnan Aziz, Margarida F. Jacome, Sarfraz Khurshid:
  Global Optimization of Compositional Systems. 93-100
  
• Hana Chockler, Eitan Farchi, Benny Godlin, Sergey Novikov:
  Cross-Entropy Based Testing. 101-108
  

Symbolic Trajectory Evaluation

• Yan Chen, Yujing He, Fei Xie, Jin Yang:
  Automatic Abstraction Refinement for Generalized Symbolic Trajectory Evaluation. 111-118
  
• Edward Smith:
  A Logic for GSTE. 119-126
  
• Sara Adams, Magnus Björk, Thomas F. Melham, Carl-Johan H. Seger:
  Automatic Abstraction in Symbolic Trajectory Evaluation. 127-135
  

Specification Theory

• Koen Claessen:
  A Coverage Analysis for Safety Property Lists. 139-145
  
• Orna Kupferman, Yoad Lustig:
  What Triggers a Behavior? 146-153
  
• Kathi Fisler:
  Two-Dimensional Regular Expressions for Compositional Bus Protocols. 154-157
  
• Martin Oberkönig, Martin Schickel, Hans Eveking:
  A Quantitative Completeness Analysis for Property-Sets. 158-161
  

Industrial-Strength Verification

• Michael L. Case, Alan Mishchenko, Robert K. Brayton:
  Automated Extraction of Inductive Invariants to Aid Model Checking. 165-172
  
• Aaron R. Bradley, Zohar Manna:
  Checking Safety by Inductive Generalization of Counterexamples to Induction. 173-180
  
• Aaron P. Hurst, Alan Mishchenko, Robert K. Brayton:
  Fast Minimum-Register Retiming via Binary Maximum-Flow. 181-187
  
• Adrian E. Seigler, Gary A. Van Huben, Hari Mony:
  Formal Verification of Partial Good Self-Test Fencing Structures. 188-191
  
• Alon Flaisher, Alon Gluska, Eli Singerman:
  Case study: Integrating FV and DV in the Verification of the Intel Core^TM 2 Duo Microprocessor. 192-195
  

Reasoning about Physical Systems

• Chao Yan, Mark R. Greenstreet:
  Circuit Level Verification of a High-Speed Toggle. 199-206
  
• Mohamed H. Zaki, Ghiath Al Sammane, Sofiène Tahar, Guy Bois:
  Combining Symbolic Simulation and Interval Arithmetic for the Verification of AMS Designs. 207-215
  
• Neha Rungta, Hyrum Carroll, Eric G. Mercer, Randall J. Roper, Mark J. Clement, Quinn Snell:
  Analyzing Gene Relationships for Down Syndrome with Labeled Transition Graphs. 216-219
  

Advanced Theorem-Proving Applications

• Julien Schmaltz:
  A Formal Model of Clock Domain Crossing and Automated Verification of Time-Triggered Hardware. 223-230
  
• Lee Pike:
  Modeling Time-Triggered Protocols and Verifying Their Real-Time Schedules. 231-238
  
• Sandip Ray, Jayanta Bhadra:
  A Mechanized Refinement Framework for Analysis of Custom Memories. 239-242
  

Last update Sat May 18 09:07:13 2013 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page