Proceedings of Formal Methods in Computer Aided Design, FMCAD 2008

Table of Contents: Preface -- Conference Organization -- Invited Tutorial: Considerations in the Design and Verification of Microprocessors for Safety-Critical and Security-Critical Applications / by David Hardin, Rockwell Collins -- Invariant-Strengthened Elimination of Dependent State Elements / by Michael Case, UC Berkeley and IBM; Alan Mishchenko, UC Berkeley; Robert Brayton, UC Berkeley; Jason Baumgartner, IBM; and Hari Mony, IBM -- Optimal Constraint-Preserving Netlist Simplification / by Jason Baumgartner, IBM; Hari Mony, IBM and University of Texas at Austin; and Adnan Aziz, University of Texas at Austin -- Recording Synthesis History for Sequential Verification / by Alan Mishchenko and Robert Brayton, UC Berkeley -- BackSpace: Formal Analysis for Post-Silicon Debug / by Flavio De Paula, Dept. of Computer Science at University of British Columbia; Marcel Gort, Dept. of Electrical & Computer Engineering at University of British Columbia; Alan Hu, Dept. of Computer Science at University of British Columbia; Steven Wilton, Dept. of Electrical & Computer Engineering at University of British Columbia; Jin Yang, Intel -- Automatic Formal Verification of Block Cipher Implementations / by Eric Whitman Smith and David Dill, Stanford University -- Verifying an Arbiter Circuit / by Chao Yan and Mark Greenstreet, University of British Columbia -- Formal Verification of Hardware Support for Advanced Encryption Standard / by Anna Slobodová, Intel -- BACH: Bounded ReachAbility CHecker for Linear Hybrid Automata / by Lei Bu, You Li, Linzhang Wang, and Xuandong Li, Nanjing University -- Going with the Flow: Parameterized Verification using Message Flows / by Murali Talupur and Mark Tuttle, Intel -- Automatic Non-Interference Lemmas for Parameterized Model Checking / by Jesse Bingham, Intel -- Model Checking Nash Equilibria in MAD Distributed Systems / by Federico Mari, Igor Melatti, Ivano Salvo, and Enrico Tronci, University of Rome; Lorenzo Alvisi, Allen Clement, and Harry Li, University of Texas at Austin -- A Theory-Based Decision Heuristic for DPLL(T) / by Dan Goldwasser, Haifa University; Ofer Strichman, Technion; Shai Fine, IBM -- A Write-Based Solver for SAT Modulo the Theory of Arrays / by Miquel Bofill, Universitat de Girona; Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, and Albert Rubio, Universitat Politécnica de Catalunya -- Scaling up the Formal Verification of Lustre Programs with SMT-based Techniques / by George Hagen and Cesare Tinelli, University of Iowa -- Word-Level Sequential Memory Abstraction for Model Checking / by Per Bjesse, Synopsys -- Combining Predicate and Numeric Abstraction for Software Model Checking / by Arie Gurfinkel and Sagar Chaki, Carnegie Mellon University -- A Refinement Approach to Design and Verification of On-Chip Communication Protocols / by Peter Böhm and Tom Melham, Oxford University -- Symbolic Program Analysis Using Term Rewriting and Generalization / by Nishant Sinha, NEC Research Labs -- Machine-Code Verification for Multiple Architectures / by Magnus Myreen and Michael Gordon, University of Cambridge; Konrad Slind, University of Utah -- Scheduling Optimisations for SPIN to Minimise Buffer Requirements in Synchronous Data Flow / by Pieter Hartel and Theo Ruys, University of Twente; Marc Geilen, Eindhoven University of Technology -- A Temporal Language for SystemC / by Deian Tabakov and Moshe Vardi, Rice University; Gila Kamhi and Eli Singerman, Intel -- Augmenting a Regular Expression-Based Temporal Logic with Local Variables / by Cindy Eisner, IBM; and Dana Fisman, IBM -- Beyond Vacuity: Towards the Strongest Passing Formula / by Hana Chockler, IBM; Ari Gurfinkel, Software Engineering Institute; Ofer Strichman, IE, Technion -- A Theory of Mutations with Applications to Vacuity, Coverage, and Fault Tolerance / by Orna Kupferman, Hebrew University; Wenchao Li and Sanjit Seshia, UC Berkeley -- Trading-Off SAT Search and Variable Quantifications for Effective Unbounded Model Checking / by G. Cabodi, P. Camurati, L. Garcia, M. Murciano, S. Nocco, and S. Quer, Politecnico di Torino -- Automatic Generation of Local Repairs for Boolean Programs / by Roopsha Samanta, Jyotirmoy Deshmukh, and E. Allen Emerson, University of Texas at Austin -- Consistency Checking of All Different Constraints over Bit-Vectors within a SAT Solver / by Armin Biere and Robert Brummayer, Johannes Kepler University -- Mechanized Information Flow Analysis through Inductive Assertions / by Warren Hunt, Jr., Robert Bellarmine Krug, Sandip Ray, and William Young, University of Texas at Austin

17-20 November, 2008 in Portland, Oregon