Synopsys Hosting Formal Methods in CAD Conference Next Week

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.