Proceedings of Formal Methods in Computer Aided Design, FMCAD 2009

Access full-text files




Formal Methods in Computer Aided Design

Journal Title

Journal ISSN

Volume Title





Table of Contents: Preface (p. v) -- Organizing Committee (p. vii) -- Program Committee (p. vii) -- Referees (p. ix) -- Keynote Presentations (p. x) -- Tutorials (p. xii) -- Industrial Experience Reports (p. xiv) -- Panels (p. xvii) -- Session 1. Model Checking -- Interpolation-Sequence Based Model Checking / by Yakir Vizel and Orna Grumberg, The Technion (p. 1) -- Structure-Aware Computation of Predicate Abstraction / by Alessandro Cimatti, FBK-irst; Jori Dubrovin, Helsinki University of Technology; Tommi Junttila, Helsinki University of Technology; and Marco Roveri, FBK-irst (p. 9) -- Enhanced Verification by Temporal Decomposition / by Michael L. Case, Hari Mony, Jason Baumgartner, and Robert Kanzelman, IBM (p. 17) -- Session 2. Software Verification -- Software Model Checking via Large-Block Encoding / by Dirk Beyer, Simon Fraser University; Alessandro Cimatti, FBK-irst; Alberto Griggio, University of Trento & Simon Fraser University; M. Erkan Keremoglu, Simon Fraser University; and Roberto Sebastiani, University of Trento (p. 25) -- Verification of Recursive Methods on Tree-like Data Structures / by Jyotirmoy Deshmukh and E. Allen Emerson, University of Texas at Austin (p. 33) -- MCC: A Runtime Verification Tool for MCAPI User Applications / by Subodh Sharma and Ganesh Gopalakrishnan, University of Utah; Eric Mercer, Brigham Young University; and Jim Holt, Freescale Semiconductor (p. 41) -- Session 3. Satisfiability Modulo Theory -- Generalized and Efficient Array Decision Procedures / by Leonardo de Moura and Nikolaj Bjørner, Microsoft Research (p. 45) -- Decision Diagrams for Linear Arithmetic / by Sagar Chaki and Arie Gurfinkel, SEI/CMU; Ofer Strichman, Technion (p. 53) -- Efficient Decision Procedure for Non-linear Arithmetic Constraints using CORDIC / by Malay Ganai and Franjo Ivančić, NEC Laboratories America (p. 61) -- Mixed Abstractions for Floating-Point Arithmetic / by Angelo Brillout, ETH Zurich; Daniel Kroening and Thomas Wahl, Oxford University (p. 69) -- Session 4. Games -- Safety First: A Two-Stage Algorithm for LTL Games / by Saqib Sohail and Fabio Somenzi, University of Colorado at Boulder (p. 77) -- Synthesizing Robust Systems / by Roderick Bloem and Karin Greimel, Graz University of Technology; Thomas Henzinger, EPFL & IST Austria; Barbara Jobstmann, EPFL (p. 85) -- Session 5. Quantitative Reasoning -- Formal Verification of Analog Designs Using MetiTarski / by William Denman, Behzad Akbarpour, and Sofiène Tahar, Concordia University, Montreal; Mohamed H. Zaki, University of British Columbia; and Lawrence Paulson, University of Cambridge (p. 93) -- Formal Verification of Correctness and Performance of Random Priority-based Arbiters / by Krishnan Kailas, IBM T.J. Watson Research Center; Viresh Paruthi and Brian Monwai, IBM Systems & Technology Group (p. 101) -- Session 6. Assume Guarantee Reasoning -- Assume-Guarantee Validation for STE Properties within an SVA Environment / by Zurab Khasidashvili and Gavriel Gavrielov, Intel Israel; and Tom Melham, Oxford University (p. 108) -- Data Mining Based Decomposition for Assume-Guarantee Reasoning / by He Zhu and Fei He, Tsinghua University; William N. N. Hung, Synopsys; Xiaoyu Song, Portland State University; and Ming Gu, Tsinghua University (p. 116) -- Session 7. Equivalence Checking -- Scalable Conditional Equivalence Checking: An Automated Invariant-Generation Based Approach / by Jason Baumgartner, Hari Mony, and Michael Case, IBM Systems & Technology Group; Jun Sawada, IBM Austin Research Laboratory; and Karen Yorav, IBM Haifa (p. 120) -- Verifying Equivalence of Memories Using a First Order Logic Theorem Prover / by Zurab Khasidashvili and Mahmoud Kinanah, Intel Israel; and Andrei Voronkov, University of Manchester (p. 128) -- A Compositional Theory for Post-Reboot Observational Equivalence Checking of Hardware / by Zurab Khasidashvili, Daher Kaiss, and Doron Bustan, Intel Israel (p. 136) -- Session 8. Debugging -- Scaling VLSI Design Debugging with Interpolation / by Brian Keng and Andreas Veneris, University of Toronto (p. 144) -- Debugging Formal Specifications Using Simple Counterstrategies / by Robert Könighofer, Georg Hofferek, and Roderick Bloem, Graz University of Technology (p. 152) -- Connecting Pre-silicon and Post-silicon Verification / by Sandip Ray and Warren Hunt, University of Texas at Austin (p. 160) -- Session 9. Case Studies and Verification in the Large -- A Verified Platform for a Gate-Level Electronic Control Unit / by Sergey Tverdyshev, Saarland University (p. 164) -- Protocol Verification Using Flows: An Industrial Experience / by John O’Leary, Murali Talupur, and Mark Tuttle, Intel (p. 172) -- Industrial Strength Refinement Checking / by Jesse Bingham, John Erickson, Gaurav Singh, and Flemming Andersen, Intel (p. 180) -- Towards a Formally Verified Network-on-Chip / by Tom van den Broek and Julien Schmaltz, Radboud University Nijmegen (p. 184) -- Hardware/Software Co-Verification of Cryptographic Algorithms using Cryptol / by Levent Erkök, Magnus Carlsson, and Adam Wick, Galois, Inc. (p. 188) -- Session 10. Synthesis -- Retiming and Resynthesis with Sweep Are Complete for Sequential Transformation / by Hai Zhou, Northwestern University (p. 192) -- SAT-Based Synthesis of Clock Gating Functions Using 3-Valued Abstraction / by Eli Arbel, Oleg Rokhlenko, and Karen Yorav, IBM Haifa (p. 198) -- Finding Heap-Bounds for Hardware Synthesis / by Byron Cook, MSR; Ashutosh Gupta, MPI-SWS; Stephen Magill, CMU; Andrey Rybalchenko, MPI-SWS; Jiri Simsa, CMU; Satnam Singh, MSR; and Viktor Vafeiadis, MSR (p. 205) -- Author Index (p. 213)
15-18 November, 2009 in Austin, Texas

LCSH Subject Headings