PROCEEDINGS OF THE 21ST CONFERENCE ON FORMAL METHODS IN COMPUTER-AIDED DESIGN – FMCAD 2021
Conference Series: Formal Methods in Computer-Aided Design, Band 2
Unser Leben ist von Hardware geprägt: Sei es der USB-Stick, der Prozessor unserer Laptops oder die Sim-Karte unseres Smartphones. Doch wer sorgt eigentlich dafür, dass diese Systeme vom ersten Entwurf an stabil und sicher funktionieren? Der Computer – mithilfe des Menschen. Das Ganze nennt sich CAD (computer-aided design=computerunterstütztes Entwerfen) und ist aus der modernen Industriewelt nicht mehr wegzudenken.
Doch wie lässt sich sicherstellen, dass eingesetzte Hardware und Computersysteme zuverlässig sind? Durch Formale Methoden: Das sind Techniken und Werkzeuge, mit denen man berechnet, ob etwa eine Systembeschreibung in sich konsistent ist oder Anforderungen richtig entworfen und implementiert wurden. Anders gesagt: Man kann damit die Sicherheit von Hardware und Software überprüfen.
Wie das konkret aussehen kann, interessiert auch die jährlich stattfindende Konferenz „Formal Methods in Computer-Aided Design (FMCAD)“. Unter der Leitung von Ruzica Piskac und Michael W. Whalen beschäftigte sich die 21. Tagung im Oktober 2021 mit den neuesten Forschungsergebnissen im Bereich der Formalen Methoden. Zu dieser Online-Tagung ist nun auch ein Konferenzband mit über 30 Beiträgen erschienen, die ein breites Spektrum der Formalen Methoden abdecken: angefangen bei der Verifikation von Hardware, nebenläufigen und verteilten Systemen und neuronalen Netzen bis hin zu maschinellem Lernen und Entscheidungsprozeduren.
Der Band gewährt einen spannenden Einblick in bahnbrechende Methoden, Technologien, theoretische Ergebnisse und Werkzeuge für Formale Logik in Rechensystemen und Systementwicklungen.
Beiträge
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
Produktinformationen
297 SeitenFormat 17,0 x 24,0 cm
ISBN: 978-3-85448-046-4
DOI: 10.34727/2021/isbn.978-3-85448-046-4
Erscheinungsdatum: Oktober 2021
Conference Series: Formal Methods in Computer-Aided Design, Band 2
Produktinformationen
Erschienen: Oktober 2021Umfang: 297 Seiten
Format: 24 x 17 cm
Sprache: Englisch
DOI: 10.34727/2021/isbn.978-3-85448-046-4
ISBN (E-Book): 978-3-85448-046-4