FMCAD 2014 - FORMAL METHODS IN COMPUTER-AIDED DESIGN CALL FOR PARTICIPATION
EPFL, Lausanne, Switzerland, October 21-24, 2014 WEB SITE INCLUDING VENUE INFORMATION: http://fmcad.org/FMCAD14 PROGRAM AND PAPERS: http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD14/advance-program.shtml DEADLINE FOR EARLY REGISTRATION (APPROACHING): Monday, 29 September 2014 PLEASE REGISTER HERE: https://www.regonline.com/FMCAD_2014 FMCAD 2014 has technical co-sponsorship from IEEE's CEDA (Council on Electronic Design Automation) and in-cooperation status with ACM SIGPLAN (Special Interest Group on Programming Languages) and ACM SIGSOFT (Special Interest Group on Software Engineering). CO-LOCATED EVENTS The following meetings will be co-located with this year's edition: -- MEMOCODE 2014, the ACM/IEEE International Conference on Formal Methods and Models for Codesign http://www.memocode-conference.com -- DIFTS 2014, International Workshop on Design and Implementation of Formal Tools and Systems http://fmgroup.polito.it/cabodi/difts2014/ PROGRAM SUMMARY: Tuesday, 21 October 09:00 Ziyad Hanna: Challenging Problems in Industrial Formal Verification 10:30 Armin Biere: Challenges in Bit-Precise Reasoning 13:45 Johannes Kinder: Efficient Symbolic Execution for Software Testing 15:45 Morgan Deters, Andrew Reynolds, Timothy King, Clark Barrett, Cesare Tinelli: A Tour of CVC4: How it works, and how to use it 18:00 Reception in Rolex Learning Center Wednesday, 22 October 08:55 Welcome from Program Chair(s) 09:00 Welcome from James Larus, dean of the EPFL School of Computer and Communication Sciences 09:05 Invited talk by Xavier Leroy: Compiler verification for fun and profit 10:45 Shilpi Goel, Warren Hunt, Matt Kaufmann and Soumava Ghosh: Simulation and Formal Verification of x86 Machine-Code Programs that make System Calls 11:15 Akash Lal and Shaz Qadeer: A Program Transformation for Faster Goal-Directed Search 13:30 Adam Walker and Leonid Ryzhyk. Predicate Abstraction for Reactive Synthesis 14:00 Adria Gascon, Ashish Tiwari, Bruno Dutertre, Pramod Subramanyan, Sharad Malik and Dejan Jovanovic. Template-based Circuit Understanding 14:30 Roderick Bloem, Georg Hofferek, Bettina Könighofer, Robert Könighofer, Simon Außerlechner and Raphael Spörk. Synthesis of Synchronization using Uninterpreted Functions 15:00 Roderick Bloem, Uwe Egly, Patrick Klampfl, Robert Koenighofer and Florian Lonsing. SAT-Based Methods for Circuit Synthesis 15:45 Gianpiero Cabodi, Marco Palena and Paolo Pasini. Interpolation with Guided Refinement: revisiting incrementality in SAT-based Unbounded Model Checking 16:15 Pavel Jancik, Jan Kofron, Simone Fulvio Rollini and Natasha Sharygina. On Interpolants and Variable Assignments 16:45 Yakir Vizel and Arie Gurfinkel. DRUPing for Interpolants Thursday, 23 October 08:00 Registration and Breakfast 09:00 Rupak Majumdar, Sai Deep Tetali and Zilong Wang. Kuai: A Model Checker for Software-defined Networks 09:30 Arie Gurfinkel, Alexander Ivrii and Anton Belov. Small Inductive Safe Invariants 10:00 Benjamin Bittner, Marco Bozzano, Alessandro Cimatti, Marco Gario and Alberto Griggio. Towards Pareto-Optimal Parameter Synthesis for Monotonic Cost Functions 10:45 Student Forum: Petr Bauch: Bit-Precise LTL Model Checking Seyedhassan Daryanavard, Thomas Marconi, Mohammad Eshghi: Design of CAD Module for JIT Extensible Processor Customized for Placement and Routing Marko Doko, Viktor Vafeiadis: Reasoning about Memory Fences in C11 Relaxed Memory Model Usman Khalid: Bayesian Networks based Probablistic Approach for Digital Circuits' Reliability Christian Krieg, Michael Rathmair, Florian Schupfer: Device Library Attack: Silently Compromising the FPGA Design Flow Siddharth Krishna: Learning Linear Invariants using Decision Trees Andrey Kupriyanov, Bernd Finkbeiner: Causality-based LTL Model Checking without Automata Michael Rathmair, Florian Schupfer: Structural System Analysis from Design Level down to Netlist Level Thorsten Tarrach: Using synthesis to fix concurrency bugs Leander Tentrup: Verifying Partial Designs with Partial Observability 13:30 Timothy King, Clark Barrett and Cesare Tinelli. Leveraging Linear and Mixed Integer Programming for SMT 14:00 Panagiotis Manolios, Vasilis Papavasileiou and Mirek Riedewald. ILP Modulo Data 14:30 Marijn Heule, Martina Seidl and Armin Biere. Efficient Extraction of Skolem Functions from QRAT Proofs 15:00 Karsten Scheibler and Bernd Becker. Using Interval Constraint Propagation for Pseudo-Boolean Constraint Solving 15:45 Andrew Reynolds, Cesare Tinelli and Leonardo De Moura. Finding Conflicting Instances of Quantified Formulas in SMT 16:15 Aina Niemetz, Mathias Preiner and Armin Biere. Turbo-Charging Lemmas on Demand with Don't Care Reasoning 16:45 Daher Kaiss and Jonathan Kalechstain. Post-silicon Timing Diagnosis Made Simple using Formal Technology 18:30 Banquet at the Olympic Museum (location) Friday, 24 October 08:00 Registration and Breakfast 09:00 Invited talk by Thomas Henzinger: Computer-Aided Verification for Biology 10:45 Xin Chen, Sriram Sankaranarayanan and Erika Abraham. Under-approximate Flowpipes for Non-linear Continuous Systems 11:15 Toni Mancini, Ivano Salvo, Federico Mari, Igor Melatti, Annalisa Massini, Stefano Sinisi, Enrico Tronci, Francesco Davi, Thomas Dierkes, Rainald Ehrig, Susanna Röblitz, Brigitte Leeners, Tillmann Kruger, Marcel Egli and Fabian Ille. Patient-Specific Models from Inter-Patient Biological Models and Clinical Records 13:30 Byron Cook, Heidy Khlaaf and Nir Piterman. Faster Temporal Reasoning for Infinite-State Programs 14:00 Brad Bingham and Mark Greenstreet. Response property checking via distributed state space exploration 14:30 Peizun Liu and Thomas Wahl. Infinite-State Backward Exploration of Boolean Broadcast Programs 15:00 Amirhossein Vakili and Nancy A. Day. Reducing CTL-live Model Checking to First-Order Logic Validity Checking 15:45 Byron Cook, Carsten Fuhs, Kaustubh Nimkar and Peter O'Hearn. Disproving termination with overapproximation 16:15 Corneliu Popeea, Andrey Rybalchenko and Andreas Wilhelm. Reduction for Compositional Verification of Multi-Threaded Programs 16:45 Sagar Chaki, Arie Gurfinkel and Nishant Sinha. Efficient Verification of Periodic Programs using Sequential Consistency and Snapshots For more details on the program and the full text of all papers, see http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD14/advance-program.shtml REGISTRATION LINK: https://www.regonline.com/FMCAD_2014
_______________________________________________ uai mailing list uai@ENGR.ORST.EDU https://secure.engr.oregonstate.edu/mailman/listinfo/uai
