Abstract is missing.
- NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical SystemsHoang-Dung Tran, Xiaodong Yang, Diego Manzanas Lopez, Patrick Musau, Luan Viet Nguyen, Weiming Xiang, Stanley Bak, Taylor T. Johnson. 3-17 [doi]
- Verification of Deep Convolutional Neural Networks Using ImageStarsHoang-Dung Tran, Stanley Bak, Weiming Xiang, Taylor T. Johnson. 18-42 [doi]
- An Abstraction-Based Framework for Neural Network VerificationYizhak Yisrael Elboher, Justin Gottschlich, Guy Katz. 43-65 [doi]
- Improved Geometric Path Enumeration for Verifying ReLU Neural NetworksStanley Bak, Hoang-Dung Tran, Kerianne Hobbs, Taylor T. Johnson. 66-96 [doi]
- Systematic Generation of Diverse Benchmarks for DNN VerificationDong Xu, David Shriver, Matthew B. Dwyer, Sebastian G. Elbaum. 97-121 [doi]
- Formal Analysis and Redesign of a Neural Network-Based Aircraft Taxiing System with VerifAIDaniel J. Fremont, Johnathan Chiu, Dragos D. Margineantu, Denis Osipychev, Sanjit A. Seshia. 122-134 [doi]
- The Move ProverJingyi Emma Zhong, Kevin Cheang, Shaz Qadeer, Wolfgang Grieskamp, Sam Blackshear, Junkil Park, Yoni Zohar, Clark W. Barrett, David L. Dill. 137-150 [doi]
- End-to-End Formal Verification of Ethereum 2.0 Deposit Smart ContractDaejun Park 0001, Yi Zhang, Grigore Rosu. 151-164 [doi]
- Stratified Abstraction of Access Control PoliciesJohn Backes, Ulises Berrueco, Tyler Bray, Daniel Brim, Byron Cook, Andrew Gacek, Ranjit Jhala, Kasper Søe Luckow, Sean McLaughlin, Madhav Menon, Daniel Peebles, Ujjwal Pugalia, Neha Rungta, Cole Schlesinger, Adam Schodde, Anvesh Tanuku, Carsten Varming, Deepa Viswanathan. 165-176 [doi]
- Synthesis of Super-Optimized Smart Contracts Using Max-SMTElvira Albert, Pablo Gordillo, Albert Rubio, Maria Anna Schett. 177-200 [doi]
- Verification of Quantitative Hyperproperties Using Trace Enumeration RelationsShubham Sahai, Pramod Subramanyan, Rohit Sinha 0001. 201-224 [doi]
- Validation of Abstract Side-Channel Models for Computer ArchitecturesHamed Nemati, Pablo Buiras, Andreas Lindner, Roberto Guanciale, Swen Jacobs. 225-248 [doi]
- Semantics, Specification, and Bounded Verification of Concurrent Libraries in Replicated SystemsKartik Nagar, Prasita Mukherjee, Suresh Jagannathan. 251-274 [doi]
- Refinement for Structured Concurrent ProgramsBernhard Kragl, Shaz Qadeer, Thomas A. Henzinger. 275-298 [doi]
- Parameterized Verification of Systems with Global Synchronization and GuardsNouraldin Jaber, Swen Jacobs, Christopher Wagner, Milind Kulkarni 0001, Roopsha Samanta. 299-323 [doi]
- Hampa: Solver-Aided Recency-Aware ReplicationXiao Li, Farzin Houshmand, Mohsen Lesani. 324-349 [doi]
- Root Causing Linearizability ViolationsBerk Çirisci, Constantin Enea, Azadeh Farzan, Suha Orhun Mutluergil. 350-375 [doi]
- Symbolic Partial-Order Execution for Testing Multi-Threaded ProgramsDaniel Schemmel, Julian Büning, César Rodríguez, David Laprell, Klaus Wehrle. 376-400 [doi]
- fault: A Python Embedded Domain-Specific Language for Metaprogramming Portable Hardware Verification ComponentsLenny Truong, Steven Herbst, Rajsekhar Setaluri, Makai Mann, Ross G. Daly, Keyi Zhang, Caleb Donovick, Daniel Stanley, Mark Horowitz, Clark W. Barrett, Pat Hanrahan. 403-414 [doi]
- Nonlinear Craig Interpolant GenerationTing Gan, Bican Xia, Bai Xue 0001, Naijun Zhan, Liyun Dai. 415-438 [doi]
- Approximate Counting of Minimal Unsatisfiable SubsetsJaroslav Bendík, Kuldeep S. Meel. 439-462 [doi]
- Tinted, Detached, and Lazy CNF-XOR Solving and Its Applications to Counting and SamplingMate Soos, Stephan Gocht, Kuldeep S. Meel. 463-484 [doi]
- Automated and Scalable Verification of Integer MultipliersMertcan Temel, Anna Slobodová, Warren A. Hunt. 485-507 [doi]
- Interpolation-Based Semantic Gate Extraction and Its Applications to QBF PreprocessingFriedrich Slivovsky. 508-528 [doi]
- TarTar: A Timed Automata Repair ToolMartin Kölbl, Stefan Leue, Thomas Wies. 529-540 [doi]
- SAW: A Tool for Safety Analysis of Weakly-Hard SystemsChao Huang, Kai-Chieh Chang, Chung-Wei Lin, Qi Zhu 0002. 543-555 [doi]
- PIRK: Scalable Interval Reachability Analysis for High-Dimensional Nonlinear SystemsAlex Devonport, Mahmoud Khaled, Murat Arcak, Majid Zamani. 556-568 [doi]
- AEON: Attractor Bifurcation Analysis of Parametrised Boolean NetworksNikola Benes, Lubos Brim, Jakub Kadlecaj, Samuel Pastva, David Safránek. 569-581 [doi]
- A Novel Approach for Solving the BMI Problem in Barrier Certificates GenerationXin Chen 0027, Chao Peng, Wang Lin, Zhengfeng Yang, Yifang Zhang, Xuandong Li. 582-603 [doi]
- Reachability Analysis Using Message Passing over Tree DecompositionsSriram Sankaranarayanan 0001. 604-628 [doi]
- Fast and Guaranteed Safe Controller Synthesis for Nonlinear Vehicle ModelsChuchu Fan, Kristina Miller, Sayan Mitra. 629-652 [doi]
- SeQuaiA: A Scalable Tool for Semi-Quantitative Analysis of Chemical Reaction NetworksMilan Ceska 0002, Calvin Chau, Jan Kretínský. 653-666 [doi]