WP_Term Object
(
    [term_id] => 14
    [name] => Synopsys
    [slug] => synopsys
    [term_group] => 0
    [term_taxonomy_id] => 14
    [taxonomy] => category
    [description] => 
    [parent] => 157
    [count] => 665
    [filter] => raw
    [cat_ID] => 14
    [category_count] => 665
    [category_description] => 
    [cat_name] => Synopsys
    [category_nicename] => synopsys
    [category_parent] => 157
)
            
arc v 800x100 High Quality (1)
WP_Term Object
(
    [term_id] => 14
    [name] => Synopsys
    [slug] => synopsys
    [term_group] => 0
    [term_taxonomy_id] => 14
    [taxonomy] => category
    [description] => 
    [parent] => 157
    [count] => 665
    [filter] => raw
    [cat_ID] => 14
    [category_count] => 665
    [category_description] => 
    [cat_name] => Synopsys
    [category_nicename] => synopsys
    [category_parent] => 157
)

Synopsys Hosting Formal Methods in CAD Conference Next Week

Synopsys Hosting Formal Methods in CAD Conference Next Week
by Bernard Murphy on 09-27-2016 at 8:00 pm

FMCAD (Formal Methods in Computer Aided Design) is a technical conference with a 20-year pedigree. This is a conference for serious formal methods teams. Key notes are from Berkeley and UCLA, committee members are all formal heavyweights and best I can tell, there is no exhibitors area.



This year, Synopsys is hosting the event at the Mountain View site, from the 3[SUP]rd[/SUP] to the 6[SUP]th[/SUP] of October.

REGISTER NOW – TIME IS LIMITED

To give you a flavor of what you can expect to hear, I detail highlights and sample papers below. One theme I personally find very interesting is growing work around CAD for networks – design and verification. This is becoming increasingly important as software-defined networking is growing. Also, the complexity of networks in industrial environments, especially given the growth of IoT, means that efficient network design, synthesis and verification is becoming a much larger problem than can be managed by current methods.

Keynotes

  • Dawn Song, professor at UC Berkeley will speak on formal verification for security – a domain that definitely needs more formal help. She’ll also discuss application domains like blockchain and smart contracts.
  • Christos Papadimitriou, professor at UC Berkeley will talk about understanding evolution through computational ideas
  • George Varghese will speak about network verification and a vision for network design automation.

Tutorials

  • Manish Pandey, leads the R&D teams for formal and static technologies, distributed systems and machine learning at Synopsys and will talk about Machine Learning and Systems for the next frontier in formal verification (should be a very interesting tutorial)
  • Pranav Ashar, CTO at Real Intent will talk about the growing importance of static methods in overall chip verification.
  • Pavol Černý, assistant professor at U Colorado Boulder will talk about program synthesis for networks (notice a theme emerging here?)
  • Bernd Finkbeiner, professor at Saarland University Germany and Markus N. Rabe, postdoc at UC Berkeley will talk about hyper-properties for hardware and how they can be verified

There’s a lengthy set of accepted papers. Topics include (this is a sample):

  • In program synthesis:

    • Synthesizing Adaptive Test Strategies from Temporal Logic Specifications

  • On hardware verification

    • Equivalence Checking Using Gröbner Bases
    • Categorical Semantics of Digital Circuits

  • On SMT solving

    • Integrating Proxy Theories and Numeric Model Lifting for Floating-Point Arithmetic
    • Accurate ICP-based Floating-Point Reasoning

  • On Protocols and architecture specifications

    • Modular Specification and Verification of a Cache-Coherent Interface
    • Trustworthy Specifications of ARM v8-A and v8-M System Level Architecture

  • On networks (there it is again!) and industrial apps

    • Combining Requirement Mining, Software Model Checking, and Simulation-Based Verification for Industrial Automotive Systems
    • Formal Verification of Division and Square Root Implementations, an Oracle Report
    • Extracting Behavior from an Executable Instruction Set Model

  • On model-checking and equivalence checking

    • Equivalence Checking By Logic Relaxation
    • Efficient Uninterpreted Function Abstraction and Refinement for Word-level Model Checking

  • On concurrent and timed systems

    • A Consistency Checker for Memory Subsystem Traces
    • Soundness of the quasi-synchronous abstraction

REGISTER NOW – TIME IS LIMITED

FMCAD are hosting a banquet on the last night at the Testarossa Winery, which I can attest is a very pleasant way to spend an evening

This event is a can’t-miss for anyone wanting to understand the frontiers in formal methods and it starts next week. Make sure you register soon.

Share this post via:

Comments

0 Replies to “Synopsys Hosting Formal Methods in CAD Conference Next Week”

You must register or log in to view/post comments.