Conference Series: Formal Methods in Computer-Aided Design, Volume 2


Our life is dominated by hardware: a USB stick, the processor in our laptops or the SIM card in our smart phone. But who or what makes sure that these systems work stably, safely and securely from the word go? The computer – with a little help from humans. The overall name for this is CAD (computer-aided design), and it’s become hard to imagine our modern industrial world without it.
So how can we be sure that the hardware and computer systems we use are reliable? By using formal methods: these are techniques and tools to calculate whether a system description is in itself consistent or whether requirements have been developed and implemented correctly. Or to put it another way: they can be used to check the safety and security of hardware and software.
Just how this works in real life was also of interest at the annual conference on “Formal Methods in Computer-Aided Design (FMCAD)”. Under the direction of Ruzica Piskac and Michael Whalen, the 21st Conference in October 2021 addressed the results of the latest research in the field of formal methods. A volume of conference proceedings with over 30 articles covering a wide range of formal methods has now been published for this online conference: starting from the verification of hardware, parallel and distributed systems as well as neuronal networks, right through to machine learning and decision-making procedures.
This volume provides a fascinating insight into revolutionary methods, technologies, theoretical results and tools for formal logic in computer systems and system developments.


Reactive Synthesis Beyond Realizability
Rayna Dimitrova

Stainless Verification System Tutorial
Viktor Kuncak and Jad Hamza

Formal Methods for the Security Analysis of Smart Contracts
Matteo Maffei

Active Automata Learning: from L* to L#
Frits Vaandrager

Invited Talks
From Viewstamped Replication to Blockchains
Barbara Liskov

Algorithms for the People
Seny Kamara

Engineering with Full-scale Formal Architecture: Morello, CHERI, Armv8-A, and RISC-V
Peter Sewell

Student Forum
The FMCAD 2021 Student Forum
Mark Santolucito

CocoAlma: A Versatile Masking Verifier
Vedad Hadžić and Roderick Bloem

End-to-End Formal Verification of a RISC-V Processor Extended with Capability Pointers
Dapeng Gao and Tom Melham

Hardware Security Leak Detection by Symbolic Simulation
Neta Bar Kama and Roope Kaivola

Scaling Up Hardware Accelerator Verification using A-QED with Functional Decomposition
Saranyu Chattopadhyay, Florian Lonsing, Luca Piccolboni, Deepraj Soni, Peng Wei, Xiaofan Zhang, Yuan Zhou, Luca Carloni, Deming Chen, Jason Cong, Ramesh Karri, Zhiru Zhang, Caroline Trippel, Clark Barrett and Subhasish Mitra

Sound and Automated Verification of Real-World RTL Multipliers
Mertcan Temel and Warren Hunt

Model Checking and IC3
IC3 with Internal Signals
Rohit Dureja, Arie Gurfinkel, Alexander Ivrii and Yakir Vizel

Single Clause Assumption without Activation Literals to Speed-up IC3
Nils Froleyks and Armin Biere

Logical Characterization of Coherent Uninterpreted Programs
Hari Govind Vediramana Krishnan, Sharon Shoham and Arie Gurfinkel

Data-driven Optimization of Inductive Generalization
Nham Le, Xujie Si and Arie Gurfinkel

Model Checking AUTOSAR Components with CBMC
Timothee Durand, Katalin Fazekas, Georg Weissenbacher and Jakob Zwirchmayr

Concurrency and Distributed Systems
Automating System Configuration
Nestan Tsiskaridze, Maxwell Strange, Makai Mann, Kavya Sreedhar, Qiaoyi Liu, Mark Horowitz and Clark Barrett

Towards an Automatic Proof of Lamport’s Paxos
Aman Goel and Karem A. Sakallah

Refinement-Based Verification of Device-to-Device Information Flow
Ning Dong, Roberto Guanciale and Mads Dam

Celestial: A Smart Contracts Verification Framework
Samvid Dharanikota, Suvam Mukherjee, Chandrika Bhardwaj, Aseem Rastogi and Akash Lal

The Civl Verifier
Bernhard Kragl and Shaz Qadeer

Applied Verification and Synthesis
Synthesizing Pareto-Optimal Interpretations for Black-Box Models
Hazem Torfah, Shetal Shah, Supratik Chakraborty, S. Akshay and Sanjit A. Seshia

Dynamic Partial Order Reduction for Spinloops
Michalis Kokologiannakis, Xiaowei Ren and Viktor Vafeiadis

Robustness between Weak Memory Models
Soham Chakraborty

Pruning and Slicing Neural Networks using Formal Verification
Ori Lahav and Guy Katz

Towards Scalable Verification of Deep Reinforcement Learning
Guy Amir, Michael Schapira and Guy Katz

SAT Solving
Exploiting Isomorphic Subgraphs in SAT
Alexander Ivrii and Ofer Strichman

On Decomposition of Maximal Satisfiable Subsets
Jaroslav Bendik

Designing Samplers is Easy: The Boon of Testers
Priyanka Golia, Mate Soos, Sourav Chakraborty and Kuldeep S. Meel

SAT-Inspired Eliminations for Superposition
Petar Vukmirović, Jasmin Blanchette and Marijn Heule

SAT Solving in the Serverless Cloud
Alex Ozdemir, Haoze Wu and Clark Barrett

SMT and First-Order Logic
Induction with Recursive Definitions in Superposition
Marton Hajdu, Petra Hozzová, Laura Kovacs and Andrei Voronkov

Fair and Adventurous Enumeration of Quantifier Instantiations
Mikolas Janota, Haniel Barbosa, Pascal Fontaine and Andrew Reynolds

Mathematical Programming Modulo Strings
Ankit Kumar and Panagiotis Manolios

Lookahead in Partitioning SMT
Antti Hyvärinen, Matteo Marescotti and Natasha Sharygina

A Multithreaded Vampire with Shared Persistent Grounding
Michael Rawson and Giles Reger

    Product information

    Publication date: October 2021
    Size: 297 pages
    Format: 24 x 17 cm
    Language: Englisch

    DOI: 10.34727/2021/isbn.978-3-85448-046-4
    ISBN (E-Book): 978-3-85448-046-4
    Added to cart.