CAV 2020: 32ND INTERNATIONAL CONFERENCE ON COMPUTER AIDED VERIFICATION

This page contains an index consisting of author-provided keywords.

A
Abstract interpretation	Reachability Analysis using Message Passing over Tree Decompositions.
abstraction	SeQuaiA: A Scalable Tool for Semi-Quantitative Analysis of Chemical Reaction Networks
Abstraction-Refinement	An Abstraction-Based Framework for Neural Network Verification
ACAS Xu	Improved Geometric Path Enumeration for Verifying ReLU Neural Networks
Access control policies	Stratified Abstraction of Access Control Policies
ACL2	Automated and Scalable Verification of Integer Multipliers
algorithm	Widest Paths and Global Propagation in Bounded Value Iteration for Stochastic Games
approximate membership query	Certifying Certainty and Uncertainty in Approximate Membership Query Structures
ApproxMC	Tinted, Detached, and Lazy CNF-XOR solving and its Applications to Counting and Sampling
Archimedean condition	Nonlinear Craig Interpolant Generation
atomic actions	Refinement for Structured Concurrent Programs
Attractors	AEON: Attractor Bifurcation Analysis of Parametrised Boolean Networks
automata	Good Enough Synthesis
automata theory	Automata Tutor v3
Automated Controller Synthesis	AMYTISS: Parallelized Automated Controller Synthesis for Large-Scale Stochastic Systems
automated testing	Formal Analysis and Redesign of a Neural Network-Based Aircraft Taxiing System with VerifAI
automaton	Widest Paths and Global Propagation in Bounded Value Iteration for Stochastic Games
autonomous systems	Formal Analysis and Redesign of a Neural Network-Based Aircraft Taxiing System with VerifAI
Axiomatic Specification	Semantics, Specification, and Bounded Verification of Concurrent Libraries in Replicated Systems
B
Barrier certificates	A Novel Approach for Solving the BMI Problem in Barrier Certicates Generation Unbounded-Time Safety Verification of Stochastic Differential Dynamics
benchmark	Systematic Generation of Diverse Benchmarks for DNN Verifiers
Bifurcation analysis	AEON: Attractor Bifurcation Analysis of Parametrised Boolean Networks
Bilinear matrix inequalities	A Novel Approach for Solving the BMI Problem in Barrier Certicates Generation
Binary Decision Diagrams	Maximum Causal Entropy Specification Inference from Demonstrations
blockchain	Formal Verification of Libra Blockchain Smart Contracts The Move Prover
bloom filters	Certifying Certainty and Uncertainty in Approximate Membership Query Structures
Boolean function synthesis	Manthan: A Data-Driven Approach for Boolean Function Synthesis
Boolean networks	AEON: Attractor Bifurcation Analysis of Parametrised Boolean Networks
Bounded Verification	Semantics, Specification, and Bounded Verification of Concurrent Libraries in Replicated Systems
Buchi objectives	Qualitative Controller Synthesis for Consumption Markov Decision Processes
Bug catching	Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic
Büchi automata	Action-Based Model Checking: Logic, Automata, and Reduction
C
CEGAR	An Abstraction-Based Framework for Neural Network Verification
CHC	Global Guidance for Local Generalization in Model Checking
Circuit Semantics	Automated and Scalable Verification of Integer Multipliers
Circuits	AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTL
Cloud computing	Stratified Abstraction of Access Control Policies
Cloud-Computing Services	AMYTISS: Parallelized Automated Controller Synthesis for Large-Scale Stochastic Systems
CNF-XOR	Tinted, Detached, and Lazy CNF-XOR solving and its Applications to Counting and Sampling
complementation	Seminator 2: Improved Semi-Determinization and Complementation of Omega-Automata
composition	Certifying Certainty and Uncertainty in Approximate Membership Query Structures
Compositional Testing	Ivy: a Multi-Modal Verification Tool for Distributed Algorithms
Computer Architecture	Automated and Scalable Verification of Integer Multipliers
Computer-aided verification	MetaVal: Witness Validation via Verification
Concurrency	Root Causing Linearizability Violations Reasoning over Permissions Regions in Concurrent Separation Logic
Concurrent Libraries	Semantics, Specification, and Bounded Verification of Concurrent Libraries in Replicated Systems
concurrent programs	Refinement for Structured Concurrent Programs
Conflict Serializability	Root Causing Linearizability Violations
Consistency	Solver-aided Recency-Aware Replicated Objects
Constrained Horn Clause	Code2Inv: A Deep Learning Framework for Program Verification
Constrained Sampling	Manthan: A Data-Driven Approach for Boolean Function Synthesis
consumption Markov decision processes	Qualitative Controller Synthesis for Consumption Markov Decision Processes
Controller Program	Towards Model Checking Real-World Software-Defined Networks
controller synthesis	Fast and Guaranteed Safe Controller Synthesis for Nonlinear Vehicle Models
Convolutional Neural Networks	Verification of Deep Convolutional Neural Networks Using ImageStars
cooperative semantics	Refinement for Structured Concurrent Programs
Cory Doctorow	Working as Intended: Surveillance Capitalism is not a Rogue Capitalism
counting	Approximate Counting of Minimal Unsatisfiable Subsets
covering array	Systematic Generation of Diverse Benchmarks for DNN Verifiers
Craig interpolant	Nonlinear Craig Interpolant Generation
Cutoffs	Parameterized Verification of Systems with Global Synchronization and Guards
Cyber-Physical Systems	Reachability Analysis using Message Passing over Tree Decompositions. NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems
D
Data Flow	AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTL
Data-driven formal methods	Manthan: A Data-Driven Approach for Boolean Function Synthesis
debugging	Formal Analysis and Redesign of a Neural Network-Based Aircraft Taxiing System with VerifAI
decidability	Decidable Synthesis of Programs with Uninterpreted Functions
deductive and statistical reasoning	Program Synthesis using Deduction-Guided Reinforcement Learning
Deductive Verication	Recursive Data Structures in SPARK
Deductive Verification	Ivy: a Multi-Modal Verification Tool for Distributed Algorithms Certifying Certainty and Uncertainty in Approximate Membership Query Structures
Deep learning	Code2Inv: A Deep Learning Framework for Program Verification
Deep Neural Networks	An Abstraction-Based Framework for Neural Network Verification
Deposit contract	End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract
diagnosis	Approximate Counting of Minimal Unsatisfiable Subsets
Discrete-Time Stochastic Systems	AMYTISS: Parallelized Automated Controller Synthesis for Large-Scale Stochastic Systems
Distributed Systems	Ivy: a Multi-Modal Verification Tool for Distributed Algorithms Solver-aided Recency-Aware Replicated Objects Parameterized Verification of Systems with Global Synchronization and Guards
domain-specific language	fault: A Python Embedded Domain-Specific Language For Metaprogramming Portable Hardware Verification Components
DTMC Model learning	Global PAC Bounds for Learning Discrete Time Markov Chains
E
educational tools	Automata Tutor v3
Efficient Verification	Automated and Scalable Verification of Integer Multipliers
electronic computer-aided design	fault: A Python Embedded Domain-Specific Language For Metaprogramming Portable Hardware Verification Components
electronic design automation	fault: A Python Embedded Domain-Specific Language For Metaprogramming Portable Hardware Verification Components
Ethereum	Synthesis of Super-Optimized Smart Contracts using Max-SMT
Explanability	Towards Robust Artificial Intelligence via Spec-consistent Machine Learning
F
Failure probability bound	Unbounded-Time Safety Verification of Stochastic Differential Dynamics
falsification	Formal Analysis and Redesign of a Neural Network-Based Aircraft Taxiing System with VerifAI
fault localization	Must Fault Localization For Program Repair
finite automata	Automata Tutor v3
Finite MDPs	AMYTISS: Parallelized Automated Controller Synthesis for Large-Scale Stochastic Systems
formal languages	Automata Tutor v3
formal methods	Probabilistic Programming: A Guide for Verificationists The Reactive Synthesis Competition (SYNTCOMP 2020)
Formal verification	Formal Verification of Libra Blockchain Smart Contracts Ivy: a Multi-Modal Verification Tool for Distributed Algorithms A Novel Approach for Solving the BMI Problem in Barrier Certicates Generation Automated and Scalable Verification of Integer Multipliers The Move Prover STMC: Statistical Model Checker with Stratified and Antithetic Sampling End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract
FPGA	RTLola Cleared for Take-Off: Monitoring Autonomous Aircraft
Frequency estimation	Global PAC Bounds for Learning Discrete Time Markov Chains
G
Gate Detection	Interpolation-Based Semantic Gate Extraction and its Applications to QBF Preprocessing
generalized Büchi automata	Seminator 2: Improved Semi-Determinization and Complementation of Omega-Automata
Graph theory	SAW: A Tool for Safety Analysis of Weakly-hard Systems
H
hardware verification	fault: A Python Embedded Domain-Specific Language For Metaprogramming Portable Hardware Verification Components
hashing-based counting	Tinted, Detached, and Lazy CNF-XOR solving and its Applications to Counting and Sampling
High Performance Computing Platform	AMYTISS: Parallelized Automated Controller Synthesis for Large-Scale Stochastic Systems
Hybrid systems	A Novel Approach for Solving the BMI Problem in Barrier Certicates Generation NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems
hyperproperties	Realizing Omega-regular Hyperproperties Verification of Quantitative Hyperproperties Using Trace Enumeration Relations
HyperQPTL	Realizing Omega-regular Hyperproperties
I
IC3	Global Guidance for Local Generalization in Model Checking PrIC3: Property Directed Reachability for MDPs
Infinite State Model Checking	Global Guidance for Local Generalization in Model Checking
Information flow security	Quantifying Information Leakage Using Model Counting Validation of Abstract Side-Channel Models for Computer Architectures
Interpolation	Global Guidance for Local Generalization in Model Checking Interpolation-Based Semantic Gate Extraction and its Applications to QBF Preprocessing
invariants	Refinement for Structured Concurrent Programs
J
just-in-time compilation	Synthesizing JIT Compilers for In-Kernel DSLs
K
knowledge base	Approximate Counting of Minimal Unsatisfiable Subsets
L
labeled transition system	Action-Based Model Checking: Logic, Automata, and Reduction
Laplace smoothing	Global PAC Bounds for Learning Discrete Time Markov Chains
layered proofs	Refinement for Structured Concurrent Programs
Learning from Demonstrations	Maximum Causal Entropy Specification Inference from Demonstrations
lexicographic	Stochastic Games with Lexicographic Reachability-Safety Objectives
Libra	The Move Prover
linear temporal logic	Action-Based Model Checking: Logic, Automata, and Reduction
linear typing	Refinement for Structured Concurrent Programs
Linearizability	Root Causing Linearizability Violations
liveness	Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling
LogicLounge	Working as Intended: Surveillance Capitalism is not a Rogue Capitalism
Loop invariant generation	Code2Inv: A Deep Learning Framework for Program Verification
LTL	Seminator 2: Improved Semi-Determinization and Complementation of Omega-Automata
M
machine learning	Towards Robust Artificial Intelligence via Spec-consistent Machine Learning NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems Formal Analysis and Redesign of a Neural Network-Based Aircraft Taxiing System with VerifAI
Markov Chain	STMC: Statistical Model Checker with Stratified and Antithetic Sampling
Markov Decision Process	Maximum Causal Entropy Specification Inference from Demonstrations Widest Paths and Global Propagation in Bounded Value Iteration for Stochastic Games
Markov Decision Processes	Optimistic Value Iteration PrIC3: Property Directed Reachability for MDPs
Max-SMT	Synthesis of Super-Optimized Smart Contracts using Max-SMT
MDPs	PrIC3: Property Directed Reachability for MDPs
Merkle tree	End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract
metaprogramming	fault: A Python Embedded Domain-Specific Language For Metaprogramming Portable Hardware Verification Components
metrics	Approximate Counting of Minimal Unsatisfiable Subsets
Microarchitectures	Validation of Abstract Side-Channel Models for Computer Architectures
minimal unsatisfiable subsets	Approximate Counting of Minimal Unsatisfiable Subsets
Mixed Monotonicity	PIRK: Scalable Interval Reachability Analysis for High-Dimensional Nonlinear Systems
Model Checking	Ivy: a Multi-Modal Verification Tool for Distributed Algorithms Towards Model Checking Real-World Software-Defined Networks Action-Based Model Checking: Logic, Automata, and Reduction TarTar: A Timed Automata Repair Tool AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTL
Model validation	Validation of Abstract Side-Channel Models for Computer Architectures
Modular Verification	Ivy: a Multi-Modal Verification Tool for Distributed Algorithms
Monte Carlo Simulation	PIRK: Scalable Interval Reachability Analysis for High-Dimensional Nonlinear Systems
multi-objective	Stochastic Games with Lexicographic Reachability-Safety Objectives
Multipliers	Automated and Scalable Verification of Integer Multipliers
MUS	Approximate Counting of Minimal Unsatisfiable Subsets
N
neural network	Systematic Generation of Diverse Benchmarks for DNN Verifiers
Neural Network Verification	Improved Geometric Path Enumeration for Verifying ReLU Neural Networks
nonlinear systems	Fast and Guaranteed Safe Controller Synthesis for Nonlinear Vehicle Models
nonlinear vehicles	Fast and Guaranteed Safe Controller Synthesis for Nonlinear Vehicle Models
O
ODE Integration	PIRK: Scalable Interval Reachability Analysis for High-Dimensional Nonlinear Systems
omega automata	Action-Based Model Checking: Logic, Automata, and Reduction
omega-automata	Seminator 2: Improved Semi-Determinization and Complementation of Omega-Automata
Omega-regular properties	Realizing Omega-regular Hyperproperties
OpenFlow	Towards Model Checking Real-World Software-Defined Networks
Optimization	Synthesis of Super-Optimized Smart Contracts using Max-SMT
ORAM verification	Verification of Quantitative Hyperproperties Using Trace Enumeration Relations
Ownership	Recursive Data Structures in SPARK
P
PAC bound	Global PAC Bounds for Learning Discrete Time Markov Chains
Parallel Algorithms	AMYTISS: Parallelized Automated Controller Synthesis for Large-Scale Stochastic Systems PIRK: Scalable Interval Reachability Analysis for High-Dimensional Nonlinear Systems
parameterized verification	Parameterized Verification of Systems with Global Synchronization and Guards Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling
Partial Order Reduction	Symbolic Partial-Order Execution for Testing Multi-Threaded Programs Towards Model Checking Real-World Software-Defined Networks Action-Based Model Checking: Logic, Automata, and Reduction
Path Enumeration	Improved Geometric Path Enumeration for Verifying ReLU Neural Networks
PDR	Global Guidance for Local Generalization in Model Checking PrIC3: Property Directed Reachability for MDPs
permissions	Reasoning over Permissions Regions in Concurrent Separation Logic
Petri Nets	AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTL
population Markov chains	SeQuaiA: A Scalable Tool for Semi-Quantitative Analysis of Chemical Reaction Networks
Predicate abstraction	Stratified Abstraction of Access Control Policies
probabilistic model checking	Optimistic Value Iteration
Probabilistic programming	Probabilistic Programming: A Guide for Verificationists
probabilistic properties	Certifying Certainty and Uncertainty in Approximate Membership Query Structures
probabilistic verification	SeQuaiA: A Scalable Tool for Semi-Quantitative Analysis of Chemical Reaction Networks PRISM-games 3.0: Stochastic Game Verification with Concurrency, Equilibria and Time
Program analysis	MetaVal: Witness Validation via Verification
Program logics	Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic
program repair	Must Fault Localization For Program Repair
program slicing	Must Fault Localization For Program Repair
program synthesis	Decidable Synthesis of Programs with Uninterpreted Functions Program Synthesis using Deduction-Guided Reinforcement Learning
program verification	Code2Inv: A Deep Learning Framework for Program Verification Nonlinear Craig Interpolant Generation
proof assistants	Certifying Certainty and Uncertainty in Approximate Membership Query Structures
Property Directed Reachability	PrIC3: Property Directed Reachability for MDPs
Q
QBF	Interpolation-Based Semantic Gate Extraction and its Applications to QBF Preprocessing
quality	Good Enough Synthesis
Quantified Boolean Formulas	Interpolation-Based Semantic Gate Extraction and its Applications to QBF Preprocessing
quantitative hyperproperties	Verification of Quantitative Hyperproperties Using Trace Enumeration Relations
quantitative logic	Good Enough Synthesis
Quantitative program analysis	Quantifying Information Leakage Using Model Counting
quantitative verification	Optimistic Value Iteration
R
reach-avoid requirements	Fast and Guaranteed Safe Controller Synthesis for Nonlinear Vehicle Models
reachability	Stochastic Games with Lexicographic Reachability-Safety Objectives
Reachability Analysis	Reachability Analysis using Message Passing over Tree Decompositions. PIRK: Scalable Interval Reachability Analysis for High-Dimensional Nonlinear Systems Verification of Deep Convolutional Neural Networks Using ImageStars
reactive synthesis	The Reactive Synthesis Competition (SYNTCOMP 2020)
Realizability	Realizing Omega-regular Hyperproperties
reasoning with permissions	Refinement for Structured Concurrent Programs
Recursive Structures	Recursive Data Structures in SPARK
Reducer	MetaVal: Witness Validation via Verification
refinement	Refinement for Structured Concurrent Programs
regular expressions	Automata Tutor v3
Reinforcement learning	Program Synthesis using Deduction-Guided Reinforcement Learning Code2Inv: A Deep Learning Framework for Program Verification
ReLU	Improved Geometric Path Enumeration for Verifying ReLU Neural Networks
repair tool	TarTar: A Timed Automata Repair Tool
Replicated Systems	Semantics, Specification, and Bounded Verification of Concurrent Libraries in Replicated Systems
Representation learning	Code2Inv: A Deep Learning Framework for Program Verification
resource-constrained systems	Qualitative Controller Synthesis for Consumption Markov Decision Processes
Robustness	Towards Robust Artificial Intelligence via Spec-consistent Machine Learning
Robustness Analysis	Verification of Deep Convolutional Neural Networks Using ImageStars
Root Causing	Root Causing Linearizability Violations
Runge-Kutta Method	PIRK: Scalable Interval Reachability Analysis for High-Dimensional Nonlinear Systems
Runtime Verification	RTLola Cleared for Take-Off: Monitoring Autonomous Aircraft
S
safety	Stochastic Games with Lexicographic Reachability-Safety Objectives
Safety verification	SAW: A Tool for Safety Analysis of Weakly-hard Systems
sampling	Tinted, Detached, and Lazy CNF-XOR solving and its Applications to Counting and Sampling
SAT	Interpolation-Based Semantic Gate Extraction and its Applications to QBF Preprocessing
satisfiability	Fast and Guaranteed Safe Controller Synthesis for Nonlinear Vehicle Models
Satisfiability modulo theories	Stratified Abstraction of Access Control Policies
SDN debugging	Towards Model Checking Real-World Software-Defined Networks
security verification	Verification of Quantitative Hyperproperties Using Trace Enumeration Relations
semi-definite programming	Nonlinear Craig Interpolant Generation
semi-deterministic	Seminator 2: Improved Semi-Determinization and Complementation of Omega-Automata
separation logic	Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic Reasoning over Permissions Regions in Concurrent Separation Logic
Side channel	Quantifying Information Leakage Using Model Counting
Side channels	Validation of Abstract Side-Channel Models for Computer Architectures
simple stochastic games	Stochastic Games with Lexicographic Reachability-Safety Objectives
simulation	Formal Analysis and Redesign of a Neural Network-Based Aircraft Taxiing System with VerifAI
Smart contract	Formal Verification of Libra Blockchain Smart Contracts
smart contracts	Synthesis of Super-Optimized Smart Contracts using Max-SMT The Move Prover End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract
SMT	Synthesis of Super-Optimized Smart Contracts using Max-SMT
SMT solving	TarTar: A Timed Automata Repair Tool
SMT-based Symbolic Model Checking	Global Guidance for Local Generalization in Model Checking
Software Testing	Symbolic Partial-Order Execution for Testing Multi-Threaded Programs
software tool	NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems
Software verification	MetaVal: Witness Validation via Verification
Software-Defined Network Verification	Towards Model Checking Real-World Software-Defined Networks
Software-defined Networks	AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTL
Spacer	Global Guidance for Local Generalization in Model Checking
Specification Inference	Maximum Causal Entropy Specification Inference from Demonstrations
Specification-based testing	Ivy: a Multi-Modal Verification Tool for Distributed Algorithms
Star Set	Improved Geometric Path Enumeration for Verifying ReLU Neural Networks
Statistical Model Checking	Global PAC Bounds for Learning Discrete Time Markov Chains STMC: Statistical Model Checker with Stratified and Antithetic Sampling
Stochastic Differential Equations (SDEs)	Unbounded-Time Safety Verification of Stochastic Differential Dynamics
stochastic game	Widest Paths and Global Propagation in Bounded Value Iteration for Stochastic Games
stochastic games	PRISM-games 3.0: Stochastic Game Verification with Concurrency, Equilibria and Time
stochastic systems	Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling
strategy synthesis	PRISM-games 3.0: Stochastic Game Verification with Concurrency, Equilibria and Time Qualitative Controller Synthesis for Consumption Markov Decision Processes
Stream Monitoring	RTLola Cleared for Take-Off: Monitoring Autonomous Aircraft
sum of squares	Nonlinear Craig Interpolant Generation
symbolic execution	Symbolic Partial-Order Execution for Testing Multi-Threaded Programs Synthesizing JIT Compilers for In-Kernel DSLs
synthesis	Solver-aided Recency-Aware Replicated Objects Synthesizing JIT Compilers for In-Kernel DSLs Synthesis of Super-Optimized Smart Contracts using Max-SMT Good Enough Synthesis The Reactive Synthesis Competition (SYNTCOMP 2020)
T
teaching	Automata Tutor v3
Temporal Logic	Ivy: a Multi-Modal Verification Tool for Distributed Algorithms STMC: Statistical Model Checker with Stratified and Antithetic Sampling AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTL
Temporal logic formulas	Global PAC Bounds for Learning Discrete Time Markov Chains
Testing	Root Causing Linearizability Violations Validation of Abstract Side-Channel Models for Computer Architectures fault: A Python Embedded Domain-Specific Language For Metaprogramming Portable Hardware Verification Components
timed automata	TarTar: A Timed Automata Repair Tool
tool	Seminator 2: Improved Semi-Determinization and Complementation of Omega-Automata
Transfer learning	Code2Inv: A Deep Learning Framework for Program Verification
translator	Seminator 2: Improved Semi-Determinization and Complementation of Omega-Automata
Tree Decompositions	Reachability Analysis using Message Passing over Tree Decompositions.
Turing machines	Automata Tutor v3
U
Unbounded safety verification	Unbounded-Time Safety Verification of Stochastic Differential Dynamics
UniGen	Tinted, Detached, and Lazy CNF-XOR solving and its Applications to Counting and Sampling
uninterpreted programs	Decidable Synthesis of Programs with Uninterpreted Functions
V
Validation of verification results	MetaVal: Witness Validation via Verification
value iteration	Optimistic Value Iteration Widest Paths and Global Propagation in Bounded Value Iteration for Stochastic Games
verification	Probabilistic Programming: A Guide for Verificationists Systematic Generation of Diverse Benchmarks for DNN Verifiers TarTar: A Timed Automata Repair Tool Reasoning over Permissions Regions in Concurrent Separation Logic An Abstraction-Based Framework for Neural Network Verification Verification of Deep Convolutional Neural Networks Using ImageStars
Verification witnesses	MetaVal: Witness Validation via Verification
Vienna Center for Logic and Algorithms at TU Wien	Working as Intended: Surveillance Capitalism is not a Rogue Capitalism
W
Weak Consistency	Semantics, Specification, and Bounded Verification of Concurrent Libraries in Replicated Systems
Weakly-hard systems	SAW: A Tool for Safety Analysis of Weakly-hard Systems
widest path problem	Widest Paths and Global Propagation in Bounded Value Iteration for Stochastic Games
Z
zero-knowledge proof verification	Verification of Quantitative Hyperproperties Using Trace Enumeration Relations

Disclaimer | Powered by EasyChair Smart Program