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.
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.
- 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.
- 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
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: