Show simple item record

dc.contributor.editorBiere, Arminen
dc.contributor.editorPixley, Carlen
dc.creatorFormal Methods in Computer Aided Designen
dc.date.accessioned2013-05-10T14:14:10Zen
dc.date.available2013-05-10T14:14:10Zen
dc.date.issued2009en
dc.identifier.isbn978-1-4244-4966-8en
dc.identifier.urihttp://hdl.handle.net/2152/20110en
dc.descriptionTable 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)en
dc.description15-18 November, 2009 in Austin, Texasen
dc.description.sponsorshipIEEE, IBM, Intel, Jasper Design Automation, NEC Labs America, NVIDIAen
dc.description.urihttp://www.cs.utexas.edu/users/hunt/FMCAD/en
dc.language.isoengen
dc.publisherIEEEen
dc.subjectcomputer scienceen
dc.subjectcomputer aided designen
dc.subjectfmcaden
dc.subjectFMCADen
dc.subjectmodel checkingen
dc.subjectsoftware verificationen
dc.subjectsatisfiability modulo theoryen
dc.subjectgamesen
dc.subjectquantitative reasoningen
dc.subjectequivalence checkingen
dc.subjectdebuggingen
dc.subjectsynthesisen
dc.titleProceedings of Formal Methods in Computer Aided Design, FMCAD 2009en
dc.typeConference Proceedingsen
dc.description.departmentComputer Sciencesen


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record