| Vedad Hadžić and Roderick Bloem |
Coco-Alma: A Versatile Masking Verifier |
Video |
Slides |
| Rohit Dureja, Arie Gurfinkel, Alexander Ivrii and Yakir Vizel |
IC3 with Internal Signals |
Video |
Slides |
| Hari Govind Vediramana Krishnan, Sharon Shoham and Arie Gurfinkel |
Logical Characterization of Coherent Uninterpreted Programs |
Video |
Slides |
| Dapeng Gao and Tom Melham |
End-to-End Formal Verification of a RISC-V Processor Extended with Capability Pointers |
Video |
Slides |
| Neta Bar Kama and Roope Kaivola |
Hardware Security Leak Detection by Symbolic Simulation |
Video |
Slides |
| Alexander Ivrii and Ofer Strichman |
Exploiting Isomorphic Subgraphs in SAT |
Video |
Slides |
| Marton Hajdu, Petra Hozzová, Laura Kovacs and Andrei Voronkov |
Induction with Recursive Definitions in Superposition |
Video |
Slides |
| Nham Le, Xujie Si and Arie Gurfinkel |
Data-driven Inductive Generalization |
Video |
Slides |
| Ori Lahav and Guy Katz |
Pruning and Slicing Neural Networks using Formal Verification |
Video |
Slides |
| 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 |
Scaling Up Hardware Accelerator Verification using A-QED with Functional Decomposition |
Video |
Slides |
| Timothee Durand, Katalin Fazekas, Georg Weissenbacher and Jakob Zwirchmayr |
Model Checking AUTOSAR Components with CBMC |
Video |
Slides |
| Jaroslav Bendík |
On Decomposition of Maximal Satisfiable Subsets |
Video |
Slides |
| Nils Froleyks and Armin Biere |
Single Clause Assumption without Activation Literals to Speed-up IC3 |
Video |
Slides |
| Hazem Torfah, Shetal Shah, Supratik Chakraborty, S. Akshay and Sanjit A. Seshia |
Synthesizing Pareto-optimal Interpretations for Black-Box Models |
Video |
Slides |
| Michalis Kokologiannakis, Xiaowei Ren and Viktor Vafeiadis |
Dynamic Partial Order Reductions for Spinloops |
Video |
Slides |
| Bernhard Kragl and Shaz Qadeer |
The Civl Verifier |
Video |
Slides |
| Mertcan Temel and Warren Hunt |
Sound and Automated Verification of Real-World RTL Multipliers |
Video |
Slides |
| Priyanka Golia, Mate Soos, Sourav Chakraborty and Kuldeep S. Meel |
Designing Samplers is Easy: The Boon of Testers |
Video |
Slides |
| Petar Vukmirović, Jasmin Blanchette and Marijn Heule |
SAT-Inspired Eliminations for Superposition |
Video |
Slides |
| Nestan Tsiskaridze, Maxwell Strange, Makai Mann, Kavya Sreedhar, Qiaoyi Liu, Mark Horowitz and Clark Barrett |
Automating System Configuration |
Video |
Slides |
| Mikolas Janota, Haniel Barbosa, Pascal Fontaine and Andrew Reynolds |
Fair and Adventurous Enumeration of Quantifier Instantiations |
Video |
Slides |
| Ankit Kumar and Panagiotis Manolios |
Mathematical Programming Modulo Strings |
Video |
Slides |
| Aman Goel and Karem A. Sakallah |
Towards an Automatic Proof of Lamport’s Paxos |
Video |
Slides |
| Antti Hyvärinen, Matteo Marescotti and Natasha Sharygina |
Lookahead in Partitioning SMT |
Video |
Slides |
| Alex Ozdemir, Haoze Wu and Clark Barrett |
SAT Solving in the Serverless Cloud |
Video |
Slides |
| Ning Dong, Roberto Guanciale and Mads Dam |
Refinement-Based Verification of Device-to-Device Information Flow |
Video |
Slides |
| Guy Amir, Michael Schapira and Guy Katz |
Towards scalable verification of deep reinforcement learning |
Video |
Slides |
| Samvid Dharanikota, Suvam Mukherjee, Chandrika Bhardwaj, Aseem Rastogi and Akash Lal |
Celestial: A Framework for Verified Smart Contracts |
Video |
Slides |
| Soham Chakraborty |
Robustness between Weak Memory Models |
Video |
Slides |
| Michael Rawson and Giles Reger |
A Multithreaded Vampire with Shared Persistent Grounding |
Video |
Slides |
