Proceedings of Formal Methods in Computer-Aided Design, FMCAD 2016
Access full-text files
Date
2016-10
Authors
Formal Methods in Computer Aided Design
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
Department
Description
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)