- Verification of Deep Convolutional Neural Networks Using ImageStars, Hoang-Dung Tran, Stanley Bak, Weiming Xiang and Taylor T Johnson
- An Abstraction-Based Framework for Neural Network Verification, Yizhak Elboher, Justin Gottschlich and Guy Katz
- Recursive Data Structures in SPARK, Claire Dross and Johannes Kanig
- Stratified Abstraction of Access Control Policies, John Backes, Ulises Berrueco, Tyler Bray, Daniel Brim, Byron Cook, Andrew Gacek, Ranjit Jhala, Kasper Luckow, Sean Mclaughlin, Madhav Menon, Daniel Peebles, Ujjwal Pugalia, Neha Rungta, Cole Schlesinger, Adam Schodde, Anvesh Tanuku, Carsten Varming and Deepa Viswanathan
- STMC: Statistical Model Checker with Stratified and Antithetic Sampling, Nima Roohi, Yu Wang, Matthew West, Geir Dullerud and Mahesh Viswanathan
- Widest Paths and Global Propagation in Bounded Value Iteration for Stochastic Games, Kittiphon Phalakarn, Toru Takisaka, Thomas Haas and Ichiro Hasuo
- Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling, Michael Blondin, Javier Esparza, Martin Helfrich, Antonín Kučera and Philipp J. Meyer
- Verification of Quantitative Hyperproperties Using Trace Enumeration Relations, Shubham Sahai, Rohit Sinha and Pramod Subramanyan
- Improved Geometric Path Enumeration for Verifying ReLU Neural Networks, Stanley Bak, Hoang Dung Tran, Kerianne Hobbs and Taylor T Johnson
- Nonlinear Craig Interpolant Generation, Ting Gan, Bican Xia, Bai Xue, Naijun Zhan and Liyun Dai
- The Move Prover, Jingyi Emma Zhong, Kevin Cheang, Shaz Qadeer, Wolfgang Grieskamp, Sam Blackshear, Junkil Park, Yoni Zohar, Clark Barrett and David Dill
- Maximum Causal Entropy Specification Inference from Demonstrations, Marcell Vazquez-Chanlatte and Sanjit A. Seshia
- Automated and Scalable Verification of Integer Multipliers, Mertcan Temel, Anna Slobodova and Warren Hunt
- Certifying Certainty and Uncertainty in Approximate Membership Query Structures, Kiran Gopinathan and Ilya Sergey
- fault: A Python Embedded Domain-Specific Language For Metaprogramming Portable Hardware Verification Components, Lenny Truong, Steven Herbst, Rajsekhar Setaluri, Makai Mann, Ross Daly, Keyi Zhang, Caleb Donovick, Daniel Stanley, Mark Horowitz, Clark Barrett and Pat Hanrahan
- End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract, Daejun Park, Yi Zhang and Grigore Rosu
- Semantics, Specification, and Bounded Verification of Concurrent Libraries in Replicated Systems, Kartik Nagar, Prasita Mukherjee and Suresh Jagannathan
- Good Enough Synthesis, Shaull Almagor and Orna Kupferman
- Approximate Counting of Minimal Unsatisfiable Subsets, Jaroslav Bendík and Kuldeep S. Meel
- AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTL, Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch and Ernst-Ruediger Olderog
- Validation of Abstract Side-Channel Models for Computer Architectures, Pablo Buiras, Roberto Guanciale, Swen Jacobs, Andreas Lindner and Hamed Nemati
- Interpolation-Based Semantic Gate Extraction and its Applications to QBF Preprocessing, Friedrich Slivovsky
- Realizing Omega-regular Hyperproperties, Bernd Finkbeiner, Christopher Hahn, Jana Hofmann and Leander Tentrup
- Reasoning over Permissions Regions in Concurrent Separation Logic, James Brotherston, Diana Costa, Aquinas Hobor and John Wickerson
- Automata Tutor v3, Loris D’Antoni, Martin Helfrich, Jan Kretinsky, Emanuel Ramneantu and Maximilian Weininger
- TarTar: A Timed Automata Repair Tool, Martin Kölbl, Stefan Leue and Thomas Wies
- Unbounded-Time Safety Verification of Stochastic Differential Dynamics, Shenghua Feng, Mingshuai Chen, Bai Xue, Sriram Sankaranarayanan and Naijun Zhan
- Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic, Azalea Raad, Josh Berdine, Hoang-Hai Dang, Derek Dreyer, Peter O’Hearn and Jules Villard
- Code2Inv: A Deep Learning Framework for Program Verification, Xujie Si, Aaditya Naik, Hanjun Dai, Mayur Naik and Le Song
- Synthesis of Super-Optimized Smart Contracts using Max-SMT, Elvira Albert, Pablo Gordillo, Albert Rubio and Maria A Schett
- Formal Analysis and Redesign of a Neural Network-Based Aircraft Taxiing System with VerifAI, Daniel J. Fremont, Johnathan Chiu, Dragos D. Margineantu, Denis Osipychev and Sanjit A. Seshia
- PrIC3: Property Directed Reachability for MDPs, Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja and Philipp Schröer
- NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems, Hoang Dung Tran, Xiaodong Yang, Diego Manzanas, Patrick Musau, Luan Nguyen, Weiming Xiang, Stanley Bak and Taylor T Johnson
- Action-Based Model Checking: Logic, Automata, and Reduction, Stephen F. Siegel and Yihao Yan
- PIRK: Scalable Interval Reachability Analysis for High-Dimensional Nonlinear Systems, Alex Devonport, Mahmoud Khaled, Murat Arcak and Majid Zamani
- Global Guidance for Local Generalization in Model Checking, Hari Govind Vediramana Krishnan, Yuting Chen, Sharon Shoham and Arie Gurfinkel
- Refinement for Structured Concurrent Programs, Bernhard Kragl, Shaz Qadeer and Thomas A. Henzinger
- Systematic Generation of Diverse Benchmarks for DNN Verifiers, Dong Xu, David Shriver, Matthew Dwyer and Sebastian Elbaum
- Towards Model Checking Real-World Software-Defined Networks, Vasileios Klimis, Bernhard Reus and George Parisis
- A Novel Approach for Solving the BMI Problem in Barrier Certicates Generation, Xin Chen, Chao Peng, Wang Lin, Zhengfeng Yang, Yifan Zhang and Xuandong Li
- Global PAC Bounds for Learning Discrete Time Markov Chains, Hugo Bazille, Blaise Genest, Cyrille Jegourel and Jun Sun
- Parameterized Verification of Systems with Global Synchronization and Guards, Nour Jaber, Christopher Wagner, Swen Jacobs, Milind Kulkarni and Roopsha Samanta
- RTLola Cleared for Take-Off: Monitoring Autonomous Aircraft, Jan Baumeister, Bernd Finkbeiner, Sebastian Schirmer, Maximilian Schwenger and Christoph Torens
- Accelerating Approximate Techniques for Counting and Sampling Models Through Refined CNF-XOR Solving, Mate Soos, Stephan Gocht and Kuldeep S. Meel
- Synthesizing JIT Compilers for In-Kernel DSLs, Jacob Van Geffen, Luke Nelson, Isil Dillig, Xi Wang and Emina Torlak
- Solver-aided Recency-Aware Replicated Objects, Xiao Li, Farzin Houshmand and Mohsen Lesani
- Ivy: a Multi-Modal Verification Tool for Distributed Algorithms, Kenneth McMillan and Oded Padon
- Reachability Analysis using Message Passing over Tree Decompositions, Sriram Sankaranarayanan
- Program Synthesis using Deduction-Guided Reinforcement Learning, Yanju Chen, Chenglong Wang, Osbert Bastani, Isil Dillig and Yu Feng
- Manthan: A Data Driven Approach for Skolem Function Synthesis, Priyanka Golia, Kuldeep S. Meel and Subhajit Roy
- Fast and Guaranteed Safe Controller Synthesis for Nonlinear Vehicle Models, Kristina Miller, Chuchu Fan and Sayan Mitra
- AMYTISS: Parallelized Automated Controller Synthesis for Large-Scale Stochastic Systems, Abolfazl Lavaei, Mahmoud Khaled, Sadegh Soudjani and Majid Zamani
- Decidable Synthesis of Programs with Uninterpreted Functions, Paul Krogmeier, Umang Mathur, Adithya Murali, Madhusudan Parthasarathy and Mahesh Viswanathan
- Seminator 2: Improved Semi-Determinization and Complementation of Omega-Automata, František Blahoudek, Alexandre Duret-Lutz and Jan Strejček
- Root Causing Linearizability Violations, Berk Çirisci, Constantin Enea, Azadeh Farzan and Suha Orhun Mutluergil
- Qualitative Controller Synthesis for Consumption Markov Decision Processes, František Blahoudek, Tomáš Brázdil, Petr Novotný, Melkior Ornik, Pranay Thangeda and Ufuk Topcu
- Symbolic Partial-Order Execution for Testing Multi-Threaded Programs, Daniel Schemmel, Julian Büning, César Rodríguez, David Laprell and Klaus Wehrle
- SAW: A Tool for Safety Analysis of Weakly-hard Systems, Chao Huang, Kai-Chieh Chang, Chung-Wei Lin and Qi Zhu
- PRISM-games 3.0: Stochastic Game Verification with Concurrency, Equilibria and Time, Marta Kwiatkowska, Gethin Norman, David Parker and Gabriel Santos
- Stochastic Games with Lexicographic Reachability-Safety Objectives, Krishnendu Chatterjee, Joost-Pieter Katoen, Maximilian Weininger and Tobias Winkler
- Must Fault Localization For Program Repair, Bat-Chen Rothenberg and Orna Grumberg
- Optimistic Value Iteration, Arnd Hartmanns and Benjamin Lucien Kaminski
- SeQuaiA: A Scalable Tool for Semi-Quantitative Analysis of Chemical Reaction Networks, Milan Ceska, Calvin Chau and Jan Kretinsky
- MetaVal: Witness Validation via Verification, Dirk Beyer and Martin Spiessl
- AEON: Attractor Bifurcation Analysis of Parametrised Boolean Networks, Nikola Benes, Lubos Brim, Jakub Kadlecaj, Samuel Pastva and David Šafránek