| Authors |
Title |
Slides |
| Yannan Li, Jingbo Wang and Chao Wang |
Proving Robustness of KNNs Against Adversarial Data Poisoning |
Slides
|
| Swen Jacobs, Mouhammad Sakr and Marcus Völp |
Automatic Repair and Deadlock Detection for Parameterized Systems |
Slides
|
| Pamina Georgiou, Bernhard Gleiss, Ahmed Bhayat, Michael Rawson, Laura Kovacs and Giles Reger |
The Rapid Software Verification Framework |
Slides
|
| Randal Bryant |
TBUDDY: A Proof-Generating BDD Package |
Slides
|
| Andreas Lööw |
Reconciling Verified-Circuit Development and Verilog Development |
Slides
|
| Emily Yu, Nils Frolyeks, Armin Biere and Keijo Heljanko |
Stratified Certification for k-Induction |
Slides
|
| Anders Schlichtkrull, Morten Konggaard Schou, Jiri Srba and Dmitriy Traytel |
Differential Testing of Pushdown Reachability with a Formally Verified Oracle |
Slides
|
| Anvay Grover, Rüdiger Ehlers and Loris D'Antoni |
Synthesizing Transducers from Complex Specifications |
Slides
|
| Omri Isac, Clark Barrett, Min Zhang and Guy Katz |
Neural Network Verification with Proof Production |
Slides
|
| Thomas Vigouroux, Cristian Ene, David Monniaux, Laurent Mounier and Marie-Laure Potet |
BaxMC: a CEGAR approach to MAX#SAT |
Slides
|
| Tom Zelazny, Haoze Wu, Clark Barrett and Guy Katz |
On Optimizing Back-Substitution Methods for Neural Network Verification |
Slides
|
| Roope Kaivola and Neta Bar Kama |
Timed Causal Fanin Analysis for Symbolic Circuit Simulation |
Slides
|
| Divya Raghunathan, Ryan Beckett, Aarti Gupta and David Walker |
ACORN: Network Control Plane Abstraction using Route Nondeterminism |
Slides
|
| Pankaj Kumar Kalita, Miriyala Jeevan Kumar and Subhajit Roy |
Synthesis of Semantic Actions in Attribute Grammars |
Slides
|
| Mario Bucev and Viktor Kunčak |
Formally Verified Quite OK Image Format |
Slides
|
| Guy Amir, Tom Zelazny, Guy Katz and Michael Schapira |
Verification-Aided Deep Ensemble Selection |
Slides
|
| William Schultz, Ian Dardik and Stavros Tripakis |
Plain and Simple Inductive Invariant Inference for Distributed Protocols in TLA+ |
Slides
|
| Alexander Konrad, Christoph Scholl, Alireza Mahzoon, Daniel Große and Rolf Drechsler |
Divider Verification Using Symbolic Computer Algebra and Delayed Don’t Care Optimization |
Slides
|
| Ruoxi Zhang, Richard Trefler and Kedar Namjoshi |
Synthesizing Locally Symmetric Parameterized Protocols from Temporal Specifications |
Slides
|
| Jonas Haglund and Roberto Guanciale |
Formally Verified Isolation of DMA |
Slides
|
| Aarti Gupta, Roope Kaivola, Mihir Parang Mehta and Vaibhav Singh |
Error Correction Code Algorithm and Implementation Verification using Symbolic Representations |
Slides
|
| Andres Noetzli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Cesare Tinelli and Clark Barrett |
Reconstructing Fine-Grained Proofs of Complex Rewrites Using a Domain-Specific Language |
Slides
|
| Ali Ebnenasir |
Synthesizing Self-Stabilizing Parameterized Protocols with Unbounded Variables |
Slides
|
| Bengt Jonsson, Magnus Lång and Kostis Sagonas |
Awaiting for Godot: Stateless Model Checking that Avoids Executions where Nothing Happens |
Slides
|
| Oliver Flatt, Samuel Coward, Max Willsey, Zachary Tatlock and Pavel Panchekha |
Small Proofs from Congruence Closure |
Slides
|
| Evan Lohn, Chris Lambert and Marijn Heule |
Compact Symmetry Breaking for Tournaments |
Slides
|
| Adwait Godbole, Yatin A. Manerkar and Sanjit A. Seshia |
Automated Conversion of Axioms to Operational Models: Theoretical and Practical Results |
Slides
|
| Fa-Hsun Chen, Shen-Chang Huang, Yu-Cheng Lu and Tony Tan |
Reducing NEXP-complete problems to DQBF |
Slides
|
| Siddharth Priya, Xiang Zhou, Yusen Su, Yakir Vizel, Yuyan Bao and Arie Gurfinkel |
Bounded Model Checking for LLVM |
Slides
|
| Martin Blicha, Grigory Fedyukovich, Antti Hyvärinen and Natasha Sharygina |
Split Transition Power Abstraction for Unbounded Safety |
Slides
|
| Abhishek Nair, Saranyu Chattopadhyay, Haoze Wu, Alex Ozdemir and Clark Barrett |
Proof-Stitch: Proof Combination for Divide-and-Conquer SAT Solvers |
Slides
|
| Suwei Yang, Victor Liang and Kuldeep S. Meel |
INC: A Scalable Incremental Weighted Sampler |
Slides
|
| Niklas Lauffer, Beyazit Yalcinkaya, Marcell Vazquez-Chanlatte, Ameesh Shah and Sanjit A. Seshia |
Learning Deterministic Finite Automata Decompositions from Examples and Demonstrations |
Slides
|
| Nishant Kheterpal, Elanor Tang and Jean-Baptiste Jeannin |
Automating Geometric Proofs of Collision Avoidance with Active Corners |
Slides
|
| Andrew T Walter, David Greve and Panagiotis Manolios |
Enumerative Data Types with Constraints |
Slides
|
| Ross Daly, Caleb Donovick, Jack Melchert, Raj Setaluri, Nestan Tsiskaridze, Priyanka Raina, Clark Barrett and Pat Hanrahan |
Synthesizing Instruction Selection Rewrite Rules from RTL using SMT |
Slides
|
| Zafer Esen and Philipp Ruemmer |
TriCera: Verifying C Programs Using the Theory of Heaps |
Slides
|
| Karl Palmskog, Xiaomo Yao, Ning Dong, Roberto Guanciale and Mads Dam |
Foundations and Tools in HOL4 for Analysis of Microarchitectural Out-of-Order Execution |
Slides
|
| Benedikt Maderbacher and Roderick Bloem |
Reactive Synthesis Modulo Theories using Abstraction Refinement |
Slides
|
| Jakob Rath, Armin Biere and Laura Kovacs |
First-Order Subsumption via SAT Solving |
Slides
|
