PROCEEDINGS OF THE 21ST CONFERENCE ON FORMAL METHODS IN COMPUTER-AIDED DESIGN – FMCAD 2021
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.
Contents
Tutorials
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
Hardware
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
297 pagesFormat 17,0 x 24,0 cm
ISBN: 978-3-85448-046-4
DOI: 10.34727/2021/isbn.978-3-85448-046-4
Publication date: October 2021
Conference Series: Formal Methods in Computer-Aided Design, Volume 2
Product information
Publication date: October 2021Size: 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