Proceedings of Formal Methods in Computer Aided Design, FMCAD 2007

Formal Methods in Computer Aided Design

Proceedings of Formal Methods in Computer Aided Design, FMCAD 2007

Access full-text files

07fmcad.pdf (4.88 MB)

Date

2007

Authors

Formal Methods in Computer Aided Design

Publisher

IEEE

Department

Computer Sciences

Description

Table of Contents: Preface (p. xx) -- Organizing Committee (p. xxi) -- Program Committee (p. xix) -- Referees (p. xxiv) -- SAT-BASED METHODS -- Exploiting Resolution Proofs to Speed up LTL Vacuity Detection for BMC / by Jocelyn Simmonds, University of Toronto; Jessica Davies, University of Toronto; Arie Gurfinkel, SEI at Carnegie Mellon University; and Marsha Chechik, University of Toronto (p. 3) -- Improved Design Debugging using Maximum Satisfiability / by Sean Safarpour, University of Toronto; Mark Liffiton, University of Michigan; Hratch Mangassarian, University of Toronto; Andreas Veneris, University of Toronto; and Karem Sakallah, University of Michigan (p. 13) -- Industrial Strength SAT-based Alignability Algorithm for Hardware Equivalence Verification / by Daher Kaiss, Marcelo Skaba, Ziyad Hanna, and Zurah Khasidashvili, Intel IDC (p. 20) -- Boosting Verification by Automatic Tuning of Decision Procedures / by Frank Hutter, Domagoj Babic, Holger Hoos, and Alan Hu, University of British Columbia (p. 27) -- HIGH-LEVEL SYSTEM ANALYSIS -- Verifying Correctness of Transactional Memories / by Ariel Cohen, New York University; John O’Leary, Intel; Amir Pnueli, New York University; Mark Tuttle, Intel; and Lenore Zuck, University of Illinois at Chicago (p. 37) -- Algorithmic Analysis of Piecewise FIFO Systems / by Naghmeh Ghafari, University of Waterloo; Arie Gurfinkel, Carnegie Mellon University; Nils Klarlund, Google; and Richard Trefler, University of Waterloo (p. 45) -- Transaction Based Modeling and Verification of Hardware Protocol Implementations / by Xiaofang Chen, University of Utah; Steven German, IBM; and Ganesh Gopalakrishnan, University of Utah (p. 53) -- Automating Hazard Checking in Transaction-Level Microarchitecture Models / by Yogesh Mahajan and Sharad Malik, Princeton University (p. 62) -- ABSTRACTION-BASED METHODS -- Computing Abstractions by Integrating BDDs and SMT / by Roberto Cavada, FBK-irst; Alessandro Cimatti, FNK-irst; Anders Franzen, FBK-irst; Kalyanasundaram Krishnamani, TIFR-Mumbai & FBK-irst; Marco Roveri, FBK-irst; and R.K. Shyamasundar, TIFR-Mumbai (p. 69) -- Induction in CEGAR for Detecting Counterexamples / by Chao Wang, Aarti Gupta, and Franjo Ivancic, NEC Labs America (p. 77) -- Lifting Propositional Interpolants to the Word-Level / by Daniel Kroening and Georg Weissenbacher, ETH Zurich (p. 85) -- SOFTWARE ANALYSIS METHODS -- Global Optimization of Compositional Systems / by Fadi Zaraket, John Pape, Adnan Aziz, Margarida Jacome, and Sarfraz Khurshid, University of Texas at Austin (p. 93) -- Cross-Entropy Based Testing / by Hana Chockler, Benny Godlin, Eitan Farchi, and Sergey Novikov, IBM Haifa Research Laboratory (p. 101) -- SYMBOLIC TRAJECTORY EVALUATION -- Automatic Abstraction Refinement for Generalized Symbolic Trajectory Evaluation / by Yan Chen, Yujing He, and Fei Xie, Portland State University; and Jin Yang, Intel (p. 111) -- A Logic for GSTE / by Edward Smith, Oxford University (p. 119) -- Automatic Abstraction in Symbolic Trajectory Evaluation / by Sara Adams, Magnus Bjork, and Tom Melham, Oxford University; and Carl-Johan Seger, Strategic CAD Labs, Intel (p. 127) -- SPECIFICATION THEORY -- A Coverage Analysis for Safety Property Lists / by Koen Claessen, Chalmers University of Technology (p. 139) -- What Triggers a Behavior? / by Orna Kupferman and Yoad Lustig, Hebrew University (p. 146) -- Two-Dimensional Regular Expressions for Compositional Bus Protocols / by Kathi Fisler, WPI Department of Computer Science (p. 154) -- A Quantitative Completeness Analysis for Property-Sets / by Martin Oberkönig, Martin Schickel, and Hans Eveking, Darmstadt University of Technology (p. 158) -- INDUSTRIAL-STRENGTH VERIFICATION -- Automated Extraction of Inductive Invariants to Aid Model Checking / by Michael Case, Alan Mishchenko, and Robert Brayton, University of California, Berkeley (p. 165) -- Checking Safety by Inductive Generalization of Counterexamples to Induction / by Aaron Bradley and Zohar Manna, Stanford University (p. 173) -- Fast Minimum Register Retiming Via Binary Maximum-Flow / by Aaron Hurst, Alan Mishchenko, and Robert Brayton, University of California, Berkeley (p. 181) -- Formal Verification of Partial Good Self-Test Fencing Structures / by Adrian Seigler, Gary Van Huben, and Hari Mony, IBM (p. 188) -- Case Study: Integrating FV and DV within the Verification of Intel® Core ™ Microprocessor / by Alon Flaisher, Alon Gluska, and Eli Singerman, Intel (p. 192) -- REASONING ABOUT PHYSICAL SYSTEMS -- Circuit-Level Verification of a High-Speed Toggle / by Chao Yan and Mark R. Greenstreet, University of British Columbia (p. 199) -- Combining Symbolic Simulation and Interval Arithmetic for the Verification of AMS Designs / by Mohamed Zaki, Ghiath Al Sammane, and Sofiene Tahar, Concordia University, Montreal; and Guy Bois, Ecole Polytechnique de Montreal (p. 207) -- Analyzing Gene Relationships for Down Syndrome with Labeled Transitions Graphs / by Neha Rungta, Brigham Young University; Hyrum Carroll, Brigham Young University; Eric Mercer, Brigham Young University; Randall Roper, Indiana University-Purdue University Indianapolis; Mark Clement, Brigham Young University; and Quinn Snell, Brigham Young University (p. 216) -- ADVANCED THEOREM-PROVING APPLICATIONS -- A Formal Model of Clock Domain Crossing and Automated Verification of Time-Triggered Hardware / by Julien Schmaltz, Radboud University Nijmegen (p. 223) -- Modeling Time-Triggered Protocols and Verifying their Real-Time Schedules / by Lee Pike, Galois (p. 231) -- A Mechanized Refinement Framework for Analysis of Custom Memories / by Sandip Ray, University of Texas at Austin; and Jayanta Bhadra, Freescale Semiconductor (p. 239) -- Author Index (p. 243)
11-14 November, 2007 in Austin, Texas