default search action
32nd CAV 2020: Los Angeles, CA, USA
- Shuvendu K. Lahiri, Chao Wang:
Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part I. Lecture Notes in Computer Science 12224, Springer 2020, ISBN 978-3-030-53287-1
AI Verification
- Hoang-Dung Tran, Xiaodong Yang, Diego Manzanas Lopez, Patrick Musau, Luan Viet Nguyen, Weiming Xiang, Stanley Bak, Taylor T. Johnson:
NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems. 3-17 - Hoang-Dung Tran, Stanley Bak, Weiming Xiang, Taylor T. Johnson:
Verification of Deep Convolutional Neural Networks Using ImageStars. 18-42 - Yizhak Yisrael Elboher, Justin Gottschlich, Guy Katz:
An Abstraction-Based Framework for Neural Network Verification. 43-65 - Stanley Bak, Hoang-Dung Tran, Kerianne Hobbs, Taylor T. Johnson:
Improved Geometric Path Enumeration for Verifying ReLU Neural Networks. 66-96 - Dong Xu, David Shriver, Matthew B. Dwyer, Sebastian G. Elbaum:
Systematic Generation of Diverse Benchmarks for DNN Verification. 97-121 - Daniel J. Fremont, Johnathan Chiu, Dragos D. Margineantu, Denis Osipychev, Sanjit A. Seshia:
Formal Analysis and Redesign of a Neural Network-Based Aircraft Taxiing System with VerifAI. 122-134
Blockchain and Security
- Jingyi Emma Zhong, Kevin Cheang, Shaz Qadeer, Wolfgang Grieskamp, Sam Blackshear, Junkil Park, Yoni Zohar, Clark W. Barrett, David L. Dill:
The Move Prover. 137-150 - Daejun Park, Yi Zhang, Grigore Rosu:
End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract. 151-164 - John 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:
Stratified Abstraction of Access Control Policies. 165-176 - Elvira Albert, Pablo Gordillo, Albert Rubio, Maria Anna Schett:
Synthesis of Super-Optimized Smart Contracts Using Max-SMT. 177-200 - Shubham Sahai, Pramod Subramanyan, Rohit Sinha:
Verification of Quantitative Hyperproperties Using Trace Enumeration Relations. 201-224 - Hamed Nemati, Pablo Buiras, Andreas Lindner, Roberto Guanciale, Swen Jacobs:
Validation of Abstract Side-Channel Models for Computer Architectures. 225-248
Concurrency
- Kartik Nagar, Prasita Mukherjee, Suresh Jagannathan:
Semantics, Specification, and Bounded Verification of Concurrent Libraries in Replicated Systems. 251-274 - Bernhard Kragl, Shaz Qadeer, Thomas A. Henzinger:
Refinement for Structured Concurrent Programs. 275-298 - Nouraldin Jaber, Swen Jacobs, Christopher Wagner, Milind Kulkarni, Roopsha Samanta:
Parameterized Verification of Systems with Global Synchronization and Guards. 299-323 - Xiao Li, Farzin Houshmand, Mohsen Lesani:
Hampa: Solver-Aided Recency-Aware Replication. 324-349 - Berk Çirisci, Constantin Enea, Azadeh Farzan, Suha Orhun Mutluergil:
Root Causing Linearizability Violations. 350-375 - Daniel Schemmel, Julian Büning, César Rodríguez, David Laprell, Klaus Wehrle:
Symbolic Partial-Order Execution for Testing Multi-Threaded Programs. 376-400
Hardware Verification and Decision Procedures
- Lenny Truong, Steven Herbst, Rajsekhar Setaluri, Makai Mann, Ross G. Daly, Keyi Zhang, Caleb Donovick, Daniel Stanley, Mark Horowitz, Clark W. Barrett, Pat Hanrahan:
fault: A Python Embedded Domain-Specific Language for Metaprogramming Portable Hardware Verification Components. 403-414 - Ting Gan, Bican Xia, Bai Xue, Naijun Zhan, Liyun Dai:
Nonlinear Craig Interpolant Generation. 415-438 - Jaroslav Bendík, Kuldeep S. Meel:
Approximate Counting of Minimal Unsatisfiable Subsets. 439-462 - Mate Soos, Stephan Gocht, Kuldeep S. Meel:
Tinted, Detached, and Lazy CNF-XOR Solving and Its Applications to Counting and Sampling. 463-484 - Mertcan Temel, Anna Slobodová, Warren A. Hunt:
Automated and Scalable Verification of Integer Multipliers. 485-507 - Friedrich Slivovsky:
Interpolation-Based Semantic Gate Extraction and Its Applications to QBF Preprocessing. 508-528 - Martin Kölbl, Stefan Leue, Thomas Wies:
TarTar: A Timed Automata Repair Tool. 529-540
Hybrid and Dynamic Systems
- Chao Huang, Kai-Chieh Chang, Chung-Wei Lin, Qi Zhu:
SAW: A Tool for Safety Analysis of Weakly-Hard Systems. 543-555 - Alex Devonport, Mahmoud Khaled, Murat Arcak, Majid Zamani:
PIRK: Scalable Interval Reachability Analysis for High-Dimensional Nonlinear Systems. 556-568 - Nikola Benes, Lubos Brim, Jakub Kadlecaj, Samuel Pastva, David Safránek:
AEON: Attractor Bifurcation Analysis of Parametrised Boolean Networks. 569-581 - Xin Chen, Chao Peng, Wang Lin, Zhengfeng Yang, Yifang Zhang, Xuandong Li:
A Novel Approach for Solving the BMI Problem in Barrier Certificates Generation. 582-603 - Sriram Sankaranarayanan:
Reachability Analysis Using Message Passing over Tree Decompositions. 604-628 - Chuchu Fan, Kristina Miller, Sayan Mitra:
Fast and Guaranteed Safe Controller Synthesis for Nonlinear Vehicle Models. 629-652 - Milan Ceska, Calvin Chau, Jan Kretínský:
SeQuaiA: A Scalable Tool for Semi-Quantitative Analysis of Chemical Reaction Networks. 653-666
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.