Proceedings of Formal Methods in Computer Aided Design, FMCAD 2012

Table of Contents: Preface (p. iv) -- Conference Organization (p. v) -- Tutorials -- Formal Methods in Cell Biology / by Jasmin Fisher, Microsoft Research (p. 1) -- Answer Set Programming / by Torsten Schaub, University of Potsdam (p. 2) -- Formal Methods for Aerospace Applications / by Eric Feron, Georgia Tech (p. 3) -- Application of SMT Solvers to Hybrid System Verification / by Alessandro Cimatti, FBK-irst (p. 4) -- Keynote -- Algebra of Concurrent Design / by Tony Hoare, Microsoft Research (p. 5) -- Session 1. Concurrent Software Verification -- Efficient Predictive Analysis for Detecting Nondeterminism in Multi-Threaded Programs / by Arnab Sinha and Sharad Malik, Princeton University; and Aarti Gupta, NEC Laboratories America (p. 6) -- Automatic Lock Insertion in Concurrent Programs / by Vineet Kahlon, NEC Labs (p. 16) -- Muti-Pushdown Systems with Budgets / by Parosh Aziz Abdulla, Mohamed Faouzi Atig, Othmane Rezine, and Jari Stenman, Uppsala University (p. 24) -- Session 2. SAT and Model Checking Algorithms -- Quantifier Elimination by Dependency Sequents / by Eugene Goldberg and Panagiotis Manolios, Northeastern University (p. 34) -- Preprocessing Techniques for First-Order Clausification / by Krystof Hoder, University of Manchester; Zurab Khasidashvili, Intel Israel; Konstantin Korovin and Andrei Voronkov, University of Manchester (p. 44) -- A Liveness Checking Algorithm that Counts / by Koen Claessen, Chalmers University of Technology; and Niklas Sörensson, Mentor Graphics Corporation (p. 52) -- Session 3. Machine Code and Memory Verification -- A Formal Model of a Large Memory that Supports Efficient Execution / by Warren Hunt and Matt Kaufmann, University of Texas at Austin (p. 60) -- Verification with Small and Short Worlds / by Rohit Sinha and Cynthia Sturton, University of California Berkeley; Petros Maniatis, Intel Labs; Sanjit A. Seshia and David Wagner, University of California Berkeley (p. 68) -- Decompilation into Logic - Improved / by Magnus O. Myreen and Michael J.C. Gordon, University of Cambridge; and Konrad Slind, Rockwell Collins (p. 78) -- Session 4. Formal Methods for Synthesis, Test and Debug -- Complete and Effective Robustness Checking by Means of Interpolation / by Stefan Frehse, University of Bremen; Görschwin Fey, University of Bremen and German Aerospace Center; Eli Arbel and Karen Yorav, IBM Haifa; and Rolf Drechsler, University of Bremen and DFKI-GmbH (p. 82) -- Symbolically Synthesizing Small Circuits / by Rüdiger Ehlers, Saarland University; Robert Könighofer and Georg Hofferek, Graz University of Technology (p. 91) -- Automated Debugging of Missing Input Constraints in a Formal Verification Environment / by Brian Keng and Andrea Veneris, University of Toronto (p. 101) -- Session 5. Software and Behavioural Hardware Verification -- Algorithms for Software Model Checking: Predicate Abstraction vs. IMPACT / by Dirk Beyer and Philipp Wendler, University of Passau, (p. 106) -- Incremental Upgrade Checking by Means of Interpolation-based Function Summaries / by Ondrej Sery, University of Lugano and Charles University; Grigory Fedyukovich and Natasha Sharygina, Charles University (p. 114) -- Verification of Parametric System Designs / by Alessandro Cimatti, Iman Narasamdya, and Marco Roveri, FBK-irst (p. 122) -- Session 6. Formal Verification Techniques for Arithmetic Circuits and GPUs -- Deciding Floating-Point Logic with Systematic Abstraction / by Leopold Haller, University of Oxford; Alberto Griggio, FBK-irst; Martin Brain and Daniel Kroening, University of Oxford (p. 131) -- Formal Verification of Error Correcting Circuits Using Computational Algebraic Geometry / by Alexey Lyov, and Luis A. Lastras-Montaño, IBM T.J. Watson Research Center; Viresh Paruthi, Robert Shadowen, and Ali El-Zein, IBM Systems & Technology Group (p. 141) -- Symbolic Trajectory Evaluation: The Primary Validation Vehicle for Next Generation Intel® Processor Graphics FPU / by Achutha Kirankumar V. M., Aarti Gupta, and Rajnish Ghughal, Intel (p. 149) -- Session 7. Automated Abstraction/Reduction Techniques -- Enhanced Reachability Analysis via Automated Dynamic Netlist-Based Hint Generation / by Jiazhao Xu, Mark Williams, Hari Mony, and Jason Baumgartner, IBM Systems & Technology Group (p. 157) -- Oscillator Verification with Probability One / by Chao Yan, Intel; and Mark Greenstreet, University of British Columbia (p. 165) -- Lazy Abstraction and SAT-Based Reachability in Hardware Model Checking / by Yakir Vizel and Orna Grumberg, Technion; and Sharon Shoham, Academic College of Tel-Aviv-Yaffo (p. 173) -- IC3-Guided Abstraction / by Jason Baumgartner, Alexander Ivrii, Arie Matsliah, and Hari Mony, IBM (p. 182) -- Session 8. Panel Session. Model Checking in the Cloud -- Formal for Everyone - Challenges in Achievable Multicore Design and Verification / by Daryl Stewart (p. 186) -- Session 9. Solver Applications -- A Quantifier-Free SMT Encoding of Non-Linear Hybrid Automata / by Alessandro Cimatti, Sergio Mover, and Stefano Tonetta, FBK-irst (p. 187) -- Piecewise Linear Modeling of Nonlinear Devices for Formal Verification of Analog Circuits / by Yan Zhang, Sriram Sankaranarayanan, and Fabio Somenzi, University of Colorado at Boulder (p. 196) -- Forward and Backward: Bounded Model Checking of Linear Hybrid Automata from Two Directions / by Yang Yang, Lei Bu, and Xuandong Li, Nanjing University (p. 204) -- Author Index (p. 209)22-25 October, 2012 in Cambridge, UKARM, Atrenta, Centaur Technology, IBM Corporation, Intel Corporation, Jasper Design Automation, Mentor Graphics, Microsoft Research, NEC Labs America, and OneSpin Solutionshttp://www.cs.utexas.edu/users/hunt/FMCAD/Computer Science