Proceedings of Formal Methods in Computer Aided Design, FMCAD 2011

Table of Contents: Preface -- Verifying Concurrent Programs / by Aarti Gupta, NEC Laboratories America (p. 1) -- Self-timing: A Step Beyond Synchrony / by Ivan Sutherland, Portland State University (p. 2) -- IC3: Where Monolithic and Incremental Meet / by Fabio Somenzi, University of Colorado at Boulder; and Aaron R. Bradley, Summit Charter Middle School (p. 3) -- Planning for End-to-End Formal Using Simulation-Based Coverage / by Prashant Aggarwal, Oski Technology; Darrow Chu, Cadence Design Systems; Vijay Kadamby, Cisco; and Vigyan Singhal, Oski Technology (p. 9) -- Specification Based Testing with QuickCheck / by John Hughes, Chalmers University of Technology and QuviQ (p. 17) -- The Role of Human Creativity in Mechanized Verification / by J. Strother Moore (p. 18) -- Interpolants from Z3 Proofs / by Kenneth L. McMillan, Microsoft Research (p. 19) -- Effective Word-Level Interpolation for Software Verification / by Alberto Griggio, FBK-irst (p. 28) -- Accelerating MUS Extraction with Recursive Model Rotation / by Anton Belov and Joao Marques-Silva, University College Dublin (p. 37) -- Pseudo-Boolean Solving by Incremental Translation to SAT / by Panagiotis Manolios and Vasilis Papavasileiou, Northeastern University (p. 41) -- Automated Specification Analysis Using an Interactive Theorem Prover / by Harsh Raju Chamarthi and Panagiotis Manolios, Northeastern University (p. 46) -- Proving and Explaining the Unfeasibility of Message Sequence Charts for Hybrid Systems / by Alessandro Cimatti, Sergio Mover, and Stefano Tonetta, FBK-irst (p. 54) -- Post-Silicon Fault Localisation Using Maximum Satisfiability and Backbones / by Charlie Shucheng Zhu, Georg Weissenbacher, and Sharad Malik, Princeton University (p. 63) -- Algebraic Approach to Arithmetic Design Verification / by Mohamed Abdul Basith and Tariq Ahmad, University of Massachusetts Amherst; André Rossi, Université de Bretagne Sud; and Maciej Ciesielski, University of Massachusetts Amherst (p. 67) -- Time-Bounded Analysis of Real-Time Systems / by Sagar Chaki and Arie Gurfinkel, SEI/CMU; and Ofer Strichman, Technion (p. 72) -- Timing Analysis of Interrupt-Driven Programs under Context Bounds / by Jonathan Kotker, Dorsa Sadigh, and Sanjit A. Seshia, University of California Berkeley (p. 81) -- Automated Error Localization and Correction for Imperative Programs / by Robert Könighofer and Roderick Bloem, Graz University of Technology (p. 91) -- Optimal Redundancy Removal without Fixedpoint Computation / by Michael Case, Jason Baumgartner, Hari Mony, and Robert Kanzelman, IBM Systems & Technology Group (p. 101) -- Approximate Reachability with Combined Symbolic and Ternary Simulation / by Michael Case, Jason Baumgartner, Hari Mony, and Robert Kanzelman, IBM Systems & Technology Group (p. 109) -- Learning Conditional Abstractions / by Bryan A. Brady, IBM; Randal E. Bryant, Carnegie Mellon University; and Sanjit A. Seshia, University of California Berkeley (p. 116) -- Efficient Implementation of Property Directed Reachability / by Niklas Een, Alan Mishchenko, and Robert Brayton, University of California Berkeley (p. 125) -- Incremental Formal Verification of Hardware / by Hana Chockler, Alexander Ivrii, Arie Matsliah, Shiri Moran, and Ziv Nevo, IBM Haifa (p. 135) -- An Incremental Approach to Model Checking Progress Properties / by Aaron R. Bradley, Fabio Somenzi, Zyad Hassan, and Yan Zhang, University of Colorado at Boulder (p. 144) -- Hardware Model Checking: Status, Challenges, and Opportunities / by Muralidhar Talupur, Intel (p. 154) -- Realtime Regular Expressions for Analog and Mixed-Signal Assertions / by John Havlicek, and Scott Little, Freescale Semiconductor (p. 155) -- Formal Analysis of Fractional Order Systems in HOL / by Umair Siddique and Osman Hasan, National University of Sciences and Technology (p. 163) -- Static Scheduling of Latency Insensitive Designs with Lucy-n / by Louis Mandel and Florence Plateau, LRI, Université Paris-Sud; and Marc Pouzet, DI, École Normale Supérieure (p. 171) -- A Theory of Abstraction for Arrays / by Steven M. German, IBM T.J. Watson Research Center (p. 176) -- Parameterized Verification of Deadlock Freedom in Symmetric Cache Coherence Protocols / by Brad Bingham and Mark Greenstreet, University of British Columbia; and Jesse Bingham, Intel (p. 186) -- Scaling Probabilistic Timing Verification of Hardware Using Abstractions in Design Source Code / by Jayanand Asok Kumar, Lingyi Liu, and Shobha Vasudevan, University of Illinois at Urbana-Champaign (p. 196) -- Pervasive Formal Verification in Control System Design / by Lee Pike, Galois, Inc. (p. 206) -- Hybrid Verification of a Hardware Modular Reduction Engine / by Jun Sawada, IBM Austin Research Laboratory; Peter Sandon, Viresh Paruthi, Jason Baumgartner, Michael Case, and Hari Mony, IBM Systems & Technology Group (p. 207) -- Desynchronization: Design for Verification / by Sudarshan K. Srinivasan and Raj. S. Katti (p. 215) -- Hunting Deadlocks Efficiently in Microarchitectural Models of Communication Fabrics / by Freek Verbeek, Radboud University Nijmegen; and Julien Schmaltz, Open University of the Netherlands (p. 223) -- Author Index (p. 232)30 October-2 November, 2011 in Austin, TexasCentaur Technology, IBM, Intel, Jasper Design Automation, NEChttp://www.cs.utexas.edu/users/hunt/FMCAD/Computer Science