Accepted Papers

  1. Verification of Deep Convolutional Neural Networks Using ImageStars, Hoang-Dung Tran, Stanley Bak, Weiming Xiang and Taylor T Johnson
  2. An Abstraction-Based Framework for Neural Network Verification, Yizhak Elboher, Justin Gottschlich and Guy Katz
  3. Recursive Data Structures in SPARK, Claire Dross and Johannes Kanig
  4. 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
  5. STMC: Statistical Model Checker with Stratified and Antithetic Sampling, Nima Roohi, Yu Wang, Matthew West, Geir Dullerud and Mahesh Viswanathan
  6. Widest Paths and Global Propagation in Bounded Value Iteration for Stochastic Games, Kittiphon Phalakarn, Toru Takisaka, Thomas Haas and Ichiro Hasuo
  7. Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling, Michael Blondin, Javier Esparza, Martin Helfrich, Antonín Kučera and Philipp J. Meyer
  8. Verification of Quantitative Hyperproperties Using Trace Enumeration Relations, Shubham Sahai, Rohit Sinha and Pramod Subramanyan
  9. Improved Geometric Path Enumeration for Verifying ReLU Neural Networks, Stanley Bak, Hoang Dung Tran, Kerianne Hobbs and Taylor T Johnson
  10. Nonlinear Craig Interpolant Generation, Ting Gan, Bican Xia, Bai Xue, Naijun Zhan and Liyun Dai
  11. The Move Prover, Jingyi Emma Zhong, Kevin Cheang, Shaz Qadeer, Wolfgang Grieskamp, Sam Blackshear, Junkil Park, Yoni Zohar, Clark Barrett and David Dill
  12. Maximum Causal Entropy Specification Inference from Demonstrations, Marcell Vazquez-Chanlatte and Sanjit A. Seshia
  13. Automated and Scalable Verification of Integer Multipliers, Mertcan Temel, Anna Slobodova and Warren Hunt
  14. Certifying Certainty and Uncertainty in Approximate Membership Query Structures, Kiran Gopinathan and Ilya Sergey
  15. 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
  16. End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract, Daejun Park, Yi Zhang and Grigore Rosu
  17. Semantics, Specification, and Bounded Verification of Concurrent Libraries in Replicated Systems, Kartik Nagar, Prasita Mukherjee and Suresh Jagannathan
  18. Good Enough Synthesis, Shaull Almagor and Orna Kupferman
  19. Approximate Counting of Minimal Unsatisfiable Subsets, Jaroslav Bendík and Kuldeep S. Meel
  20. AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTL, Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch and Ernst-Ruediger Olderog
  21. Validation of Abstract Side-Channel Models for Computer Architectures, Pablo Buiras, Roberto Guanciale, Swen Jacobs, Andreas Lindner and Hamed Nemati
  22. Interpolation-Based Semantic Gate Extraction and its Applications to QBF Preprocessing, Friedrich Slivovsky
  23. Realizing Omega-regular Hyperproperties, Bernd Finkbeiner, Christopher Hahn, Jana Hofmann and Leander Tentrup
  24. Reasoning over Permissions Regions in Concurrent Separation Logic, James Brotherston, Diana Costa, Aquinas Hobor and John Wickerson
  25. Automata Tutor v3, Loris D’Antoni, Martin Helfrich, Jan Kretinsky, Emanuel Ramneantu and Maximilian Weininger
  26. TarTar: A Timed Automata Repair Tool, Martin Kölbl, Stefan Leue and Thomas Wies
  27. Unbounded-Time Safety Verification of Stochastic Differential Dynamics, Shenghua Feng, Mingshuai Chen, Bai Xue, Sriram Sankaranarayanan and Naijun Zhan
  28. 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
  29. Code2Inv: A Deep Learning Framework for Program Verification, Xujie Si, Aaditya Naik, Hanjun Dai, Mayur Naik and Le Song
  30. Synthesis of Super-Optimized Smart Contracts using Max-SMT, Elvira Albert, Pablo Gordillo, Albert Rubio and Maria A Schett
  31. 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
  32. PrIC3: Property Directed Reachability for MDPs, Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja and Philipp Schröer
  33. 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
  34. Action-Based Model Checking: Logic, Automata, and Reduction, Stephen F. Siegel and Yihao Yan
  35. PIRK: Scalable Interval Reachability Analysis for High-Dimensional Nonlinear Systems, Alex Devonport, Mahmoud Khaled, Murat Arcak and Majid Zamani
  36. Global Guidance for Local Generalization in Model Checking, Hari Govind Vediramana Krishnan, Yuting Chen, Sharon Shoham and Arie Gurfinkel
  37. Refinement for Structured Concurrent Programs, Bernhard Kragl, Shaz Qadeer and Thomas A. Henzinger
  38. Systematic Generation of Diverse Benchmarks for DNN Verifiers, Dong Xu, David Shriver, Matthew Dwyer and Sebastian Elbaum
  39. Towards Model Checking Real-World Software-Defined Networks, Vasileios Klimis, Bernhard Reus and George Parisis
  40. 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
  41. Global PAC Bounds for Learning Discrete Time Markov Chains, Hugo Bazille, Blaise Genest, Cyrille Jegourel and Jun Sun
  42. Parameterized Verification of Systems with Global Synchronization and Guards, Nour Jaber, Christopher Wagner, Swen Jacobs, Milind Kulkarni and Roopsha Samanta
  43. RTLola Cleared for Take-Off: Monitoring Autonomous Aircraft, Jan Baumeister, Bernd Finkbeiner, Sebastian Schirmer, Maximilian Schwenger and Christoph Torens
  44. Accelerating Approximate Techniques for Counting and Sampling Models Through Refined CNF-XOR Solving, Mate Soos, Stephan Gocht and Kuldeep S. Meel
  45. Synthesizing JIT Compilers for In-Kernel DSLs, Jacob Van Geffen, Luke Nelson, Isil Dillig, Xi Wang and Emina Torlak
  46. Solver-aided Recency-Aware Replicated Objects, Xiao Li, Farzin Houshmand and Mohsen Lesani
  47. Ivy: a Multi-Modal Verification Tool for Distributed Algorithms, Kenneth McMillan and Oded Padon
  48. Reachability Analysis using Message Passing over Tree Decompositions, Sriram Sankaranarayanan
  49. Program Synthesis using Deduction-Guided Reinforcement Learning, Yanju Chen, Chenglong Wang, Osbert Bastani, Isil Dillig and Yu Feng
  50. Manthan: A Data Driven Approach for Skolem Function Synthesis, Priyanka Golia, Kuldeep S. Meel and Subhajit Roy
  51. Fast and Guaranteed Safe Controller Synthesis for Nonlinear Vehicle Models, Kristina Miller, Chuchu Fan and Sayan Mitra
  52. AMYTISS: Parallelized Automated Controller Synthesis for Large-Scale Stochastic Systems, Abolfazl Lavaei, Mahmoud Khaled, Sadegh Soudjani and Majid Zamani
  53. Decidable Synthesis of Programs with Uninterpreted Functions, Paul Krogmeier, Umang Mathur, Adithya Murali, Madhusudan Parthasarathy and Mahesh Viswanathan
  54. Seminator 2: Improved Semi-Determinization and Complementation of Omega-Automata, František Blahoudek, Alexandre Duret-Lutz and Jan Strejček
  55. Root Causing Linearizability Violations, Berk Çirisci, Constantin Enea, Azadeh Farzan and Suha Orhun Mutluergil
  56. Qualitative Controller Synthesis for Consumption Markov Decision Processes, František Blahoudek, Tomáš Brázdil, Petr Novotný, Melkior Ornik, Pranay Thangeda and Ufuk Topcu
  57. Symbolic Partial-Order Execution for Testing Multi-Threaded Programs, Daniel Schemmel, Julian Büning, César Rodríguez, David Laprell and Klaus Wehrle
  58. SAW: A Tool for Safety Analysis of Weakly-hard Systems, Chao Huang, Kai-Chieh Chang, Chung-Wei Lin and Qi Zhu
  59. PRISM-games 3.0: Stochastic Game Verification with Concurrency, Equilibria and Time, Marta Kwiatkowska, Gethin Norman, David Parker and Gabriel Santos
  60. Stochastic Games with Lexicographic Reachability-Safety Objectives, Krishnendu Chatterjee, Joost-Pieter Katoen, Maximilian Weininger and Tobias Winkler
  61. Must Fault Localization For Program Repair, Bat-Chen Rothenberg and Orna Grumberg
  62. Optimistic Value Iteration, Arnd Hartmanns and Benjamin Lucien Kaminski
  63. SeQuaiA: A Scalable Tool for Semi-Quantitative Analysis of Chemical Reaction Networks, Milan Ceska, Calvin Chau and Jan Kretinsky
  64. MetaVal: Witness Validation via Verification, Dirk Beyer and Martin Spiessl
  65. AEON: Attractor Bifurcation Analysis of Parametrised Boolean Networks, Nikola Benes, Lubos Brim, Jakub Kadlecaj, Samuel Pastva and David Šafránek