7. FMCAD 2008: Portland, Oregon, USA

• David S. Hardin:
  Invited Tutorial: Considerations in the Design and Verification of Microprocessors for Safety-Critical and Security-Critical Applications. 1-8
  
• Michael L. Case, Alan Mishchenko, Robert K. Brayton, Jason Baumgartner, Hari Mony:
  Invariant-Strengthened Elimination of Dependent State Elements. 1-9
  
• Jason Baumgartner, Hari Mony, Adnan Aziz:
  Optimal Constraint-Preserving Netlist Simplification. 1-9
  
• Alan Mishchenko, Robert K. Brayton:
  Recording Synthesis History for Sequential Verification. 1-8
  
• Flavio M. de Paula, Marcel Gort, Alan J. Hu, Steven J. E. Wilton, Jin Yang:
  BackSpace: Formal Analysis for Post-Silicon Debug. 1-10
  
• Eric Whitman Smith, David L. Dill:
  Automatic Formal Verification of Block Cipher Implementations. 1-7
  
• Chao Yan, Mark R. Greenstreet:
  Verifying an Arbiter Circuit. 1-9
  
• Anna Slobodová:
  Formal Verification of Hardware Support for Advanced Encryption Standard. 1-4
  
• Lei Bu, You Li, Linzhang Wang, Xuandong Li:
  BACH : Bounded ReAchability CHecker for Linear Hybrid Automata. 1-4
  
• Murali Talupur, Mark R. Tuttle:
  Going with the Flow: Parameterized Verification Using Message Flows. 1-8
  
• Jesse Bingham:
  Automatic Non-Interference Lemmas for Parameterized Model Checking. 1-8
  
• Federico Mari, Igor Melatti, Ivano Salvo, Enrico Tronci, Lorenzo Alvisi, Allen Clement, Harry C. Li:
  Model Checking Nash Equilibria in MAD Distributed Systems. 1-8
  
• Dan Goldwasser, Ofer Strichman, Shai Fine:
  A Theory-Based Decision Heuristic for DPLL(T). 1-8
  
• Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio:
  A Write-Based Solver for SAT Modulo the Theory of Arrays. 1-8
  
• George Hagen, Cesare Tinelli:
  Scaling Up the Formal Verification of Lustre Programs with SMT-Based Techniques. 1-9
  
• Per Bjesse:
  Word-Level Sequential Memory Abstraction for Model Checking. 1-9
  
• Arie Gurfinkel, Sagar Chaki:
  Combining Predicate and Numeric Abstraction for Software Model Checking. 1-9
  
• Peter Böhm, Tom Melham:
  A Refinement Approach to Design and Verification of On-Chip Communication Protocols. 1-8
  
• Nishant Sinha:
  Symbolic Program Analysis Using Term Rewriting and Generalization. 1-9
  
• Magnus O. Myreen, Michael J. C. Gordon, Konrad Slind:
  Machine-Code Verification for Multiple Architectures - An Application of Decompilation into Logic. 1-8
  
• Pieter H. Hartel, Theo C. Ruys, Marc C. W. Geilen:
  Scheduling Optimisations for SPIN to Minimise Buffer Requirements in Synchronous Data Flow. 1-10
  
• Deian Tabakov, Gila Kamhi, Moshe Y. Vardi, Eli Singerman:
  A Temporal Language for SystemC. 1-9
  
• Cindy Eisner, Dana Fisman:
  Augmenting a Regular Expression-Based Temporal Logic with Local Variables. 1-8
  
• Hana Chockler, Arie Gurfinkel, Ofer Strichman:
  Beyond Vacuity: Towards the Strongest Passing Formula. 1-8
  
• Orna Kupferman, Wenchao Li, Sanjit A. Seshia:
  A Theory of Mutations with Applications to Vacuity, Coverage, and Fault Tolerance. 1-9
  
• Gianpiero Cabodi, Paolo Camurati, Luz Garcia, Marco Murciano, Sergio Nocco, Stefano Quer:
  Trading-Off SAT Search and Variable Quantifications for Effective Unbounded Model Checking. 1-8
  
• Roopsha Samanta, Jyotirmoy V. Deshmukh, E. Allen Emerson:
  Automatic Generation of Local Repairs for Boolean Programs. 1-10
  
• Armin Biere, Robert Brummayer:
  Consistency Checking of All Different Constraints over Bit-Vectors within a SAT Solver. 1-4
  
• Warren A. Hunt Jr., Robert Bellarmine Krug, Sandip Ray, William D. Young:
  Mechanized Information Flow Analysis through Inductive Assertions. 1-4