CAV 2020: 32ND INTERNATIONAL CONFERENCE ON COMPUTER AIDED VERIFICATION

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

Disclaimer | Powered by EasyChair Smart Program