Formal Methods in Computer-Aided Design, 3-6 October, 2016, Mountain View, CA, USA

Accepted Papers

Tomoya Yamaguchi, Tomoyuki Kaga, Alexandre Donzé and Sanjit A SeshiaCombining Requirement Mining, Software Model Checking, and Simulation-Based Verification for Industrial Automotive Systems
Opeoluwa Matthews, Jesse Bingham and Daniel SorinVerifiable Hierarchical Protocols with Network Invariants on Parametric Systems
Guy Katz, Clark Barrett, Cesare Tinelli, Andrew Reynolds and Liana HadareanLazy Proofs for DPLL(T)-Based SMT Solvers
Ofer Guthmann, Ofer Strichman and Anna TrostanetskiMinimal unsatisfiable core extraction for SMT
Alexander NadelRouting under Constraints
Roderick Bloem, Robert Koenighofer, Ingo Pill and Franz RoeckSynthesizing Adaptive Test Strategies from Temporal Logic Specifications
Pavel ParizekHybrid Partial Order Reduction with Under-Approximate Dynamic Points-To and Determinacy Information
Matthew Naylor, Simon Moore and Alan MujumdarA Consistency Checker for Memory Subsystem Traces
Karsten Scheibler, Felix Neubauer, Ahmed Mahdi, Martin Fränzle, Tino Teige, Tom Bienmüller, Detlef Fehrer and Bernd BeckerAccurate ICP-based Floating-Point Reasoning
Hossein Hojjat, Philipp Ruemmer, Jedidiah McClurg, Pavol Černý and Nate FosterOptimizing Horn Solvers for Network Repair
Brian Campbell and Ian StarkExtracting Behaviour from an Executable Instruction Set Model
Rohit Singh and Armando Solar-LezamaSWAPPER: A Framework for Automatic Generation of Formula Simplifiers based on Conditional Rewrite Rules
David Rager, Jo Ebergen, Dmitry Nadezhin, Austin Lee, Cuong Chau and Ben SelfridgeFormal Verification of Division and Square Root Implementations, an Oracle Report
Jaideep Ramachandran and Thomas WahlIntegrating Proxy Theories and Numeric Model Lifting for Floating-Point Arithmetic
Dejan Jovanović and Bruno DutertreProperty-Directed k-Induction
Yen-Sheng Ho, Pankaj Chauhan, Pritam Roy, Alan Mishchenko and Robert BraytonEfficient Uninterpreted Function Abstraction and Refinement for Word-level Model Checking
Guillaume Baudart, Timothy Bourke and Marc PouzetSoundness of the Quasi-Synchronous Abstraction
Ermenegildo Tomasco, Truc Nguyen Lam, Omar Inverso, Bernd Fischer, Salvatore La Torre and Gennaro ParlatoLazy Sequentialization for TSO and PSO via Shared Memory Abstractions
Alastair ReidTrustworthy Specifications of ARM v8-A and v8-M System Level Architecture
Dan Ghica and Achim JungCategorical Semantics of Digital Circuits
Alain Mebsout and Cesare TinelliProof Certificates for SMT-based Model Checkers for Infinite-state Systems
Eugene GoldbergEquivalence Checking By Logic Relaxation
Amr Sayed-Ahmed, Daniel Grosse, Mathias Soeken and Rolf DrechslerEquivalence Checking Using Gröbner Bases
Kenneth McMillanModular Specification and Verification of a Cache-Coherent Interface
Susmit Jha, Vasumathi Raman and Sanjit A. SeshiaOn ∃ ∀ ∃! Solving: A Case Study on Automated Synthesis of Magic Card Tricks
Gianpiero Cabodi, Paolo E. Camurati, Marco Palena, Paolo Pasini and Danilo VendraminettoReducing Interpolant Circuit Size by Ad Hoc Logic Synthesis and SAT-Based Weakening