Proceedings of Formal Methods in Computer-Aided Design, FMCAD 2016
MetadataShow full item record
Table of Contents: Formal Verification for Computer Security: Lessons Learned and Future Directions / by Dawn Song (p.1) --Understanding Evolution through Algorithms / by Christos Papadimitriou (p.2) -- Network Verification - When Clarke Meets Cerf / by George Varghese (p.3) -- Machine Learning and Systems for the Next Frontier in Formal Verification / by Manish Pandey (p.4) -- Verifying Hyperproperties of Hardware Systems / by Bernd Finkbeiner and Markus Rabe (p.5) -- A Paradigm Shift in Verification Methodology / by Pranav Ashar (p.6) -- Program Synthesis for Networks / by Pavol Cern ˇ y´ (p.7) -- The FMCAD 2016 Graduate Student Forum / by Hossein Hojjat (p.8) -- Soundness of the Quasi-Synchronous Abstraction / by Guillaume Baudart, Timothy Bourke and Marc Pouzet (p.9) -- Synthesizing Adaptive Test Strategies from Temporal Logic Specifications / by Roderick Bloem, Robert Koenighofer, Ingo Pill and Franz Roeck (p.17) -- Reducing Interpolant Circuit Size by Ad Hoc Logic Synthesis and SAT-Based Weakening / by Gianpiero Cabodi, Paolo E. Camurati, Marco Palena, Paolo Pasini and Danilo Vendraminetto (p.25) -- Extracting Behaviour from an Executable Instruction Set Model / by Brian Campbell and Ian Stark (p.33) -- Categorical Semantics of Digital Circuits / by Dan Ghica and Achim Jung (p.41) -- Equivalence Checking By Logic Relaxation / by Eugene Goldberg (p.49) -- Minimal unsatisfiable core extraction for SMT / by Ofer Guthmann, Ofer Strichman and Anna Trostanetski (p.57) -- Efficient Uninterpreted Function Abstraction and Refinement for Word-level Model Checking / by Yen-Sheng Ho, Pankaj Chauhan, Pritam Roy, Alan Mishchenko and Robert Brayton (p.65) -- Optimizing Horn Solvers for Network Repair / by Hossein Hojjat, Philipp Ruemmer, Jedidiah McClurg, Pavol Cerny and Nate Foster ˇ (p.73) -- On ∃∀∃! Solving: A Case Study on Automated Synthesis of Magic Card Tricks / by Susmit Jha, Vasumathi Raman and Sanjit A. Seshia (p.81) -- Property-Directed k-Induction / by Dejan Jovanovic and Bruno Dutertre ´ (p.85) -- Lazy Proofs for DPLL(T)-Based SMT Solvers / by Guy Katz, Clark Barrett, Cesare Tinelli, Andrew Reynolds and Liana Hadarean (p.93) -- Verifiable Hierarchical Protocols with Network Invariants on Parametric Systems / by Opeoluwa Matthews, Jesse Bingham and Daniel Sorin (pg.101) -- Modular Specification and Verification of a Cache-Coherent Interface / by Kenneth McMillan (p.109) -- Proof Certificates for SMT-based Model Checkers for Infinite-state Systems / by Alain Mebsout and Cesare Tinelli (p.117) -- Routing under Constraints / by Alexander Nadel (p.125) -- A Consistency Checker for Memory Subsystem Traces / by Matthew Naylor, Simon Moore and Alan Mujumdar (p.133) -- Hybrid Partial Order Reduction with Under-Approximate Dynamic Points-To and Determinacy Information / by Pavel Parizek (p.141) -- Formal Verification of Division and Square Root Implementations, an Oracle Report by / David Rager, Jo Ebergen, Dmitry Nadezhin, Austin Lee, Cuong Chau and Ben Selfridge (p.149) -- Integrating Proxy Theories and Numeric Model Lifting for Floating-Point Arithmetic / by Jaideep Ramachandran and Thomas Wahl (p.153) -- Trustworthy Specifications of ARM v8-A and v8-M System Level Architecture / by Alastair Reid (p.161) -- Equivalence Checking Using Grobner Bases / by Amr Sayed-Ahmed, Daniel Grosse, Mathias Soeken and Rolf Drechsler (p.169) -- Accurate ICP-based Floating-Point Reasoning / by Karsten Scheibler, Felix Neubauer, Ahmed Mahdi, Martin Franzle, Tino Teige, Tom Bienm ¨ uller, Detlef Fehrer and ¨ Bernd Becker (p.177) -- SWAPPER: A Framework for Automatic Generation of Formula Simplifiers based on Conditional Rewrite Rules / by Rohit Singh and Armando Solar-Lezama (p.185) -- Lazy Sequentialization for TSO and PSO via Shared Memory Abstractions / by Ermenegildo Tomasco, Truc Nguyen Lam, Omar Inverso, Bernd Fischer, Salvatore La Torre and Gennaro Parlato (p.193) -- Combining Requirement Mining, Software Model Checking, and Simulation-Based Verification for Industrial Automotive Systems/ by Tomoya Yamaguchi, Tomoyuuki Kaga, Alexandre Donze and Sanjit A Seshia (p.201)
Showing items related by title, author, creator and subject.
Gansky, Andrew Emil (2017-05)Apple, Inc. is today one of the wealthiest and most powerful corporations in the world, with annual revenues that rival the gross domestic products of nations such as New Zealand. Over the company’s four-decade history, ...
Isen, Ciji (2011-05)The trends in virtualization as well as multi-core, multiprocessor environments have translated to a massive increase in the amount of main memory each individual system needs to be fitted with, so as to effectively ...