Show simple item record

dc.creatorFormal Methods in Computer Aided Designen
dc.date.accessioned2013-05-13T16:18:26Zen
dc.date.available2013-05-13T16:18:26Zen
dc.date.issued2012en
dc.identifier.urihttp://hdl.handle.net/2152/20115en
dc.descriptionTable 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)en
dc.description22-25 October, 2012 in Cambridge, UKen
dc.description.sponsorshipARM, Atrenta, Centaur Technology, IBM Corporation, Intel Corporation, Jasper Design Automation, Mentor Graphics, Microsoft Research, NEC Labs America, and OneSpin Solutionsen
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.subjectsoftware verificationen
dc.subjectmodel checking algorithmsen
dc.subjectmemory verificationen
dc.subjecthardware verificationen
dc.titleProceedings of Formal Methods in Computer Aided Design, FMCAD 2012en
dc.typeConference Proceedingsen
dc.description.departmentComputer Sciencesen


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record