CAV 2019: 31ST INTERNATIONAL CONFERENCE ON COMPUTER AIDED VERIFICATION

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

A
Abstract interpretation	Loop Summarization with Rational Vector Addition Systems
Abstract Transformers	Verifying Asynchronous Event-Driven Programs Using Partial Abstract Transformers
affine loops	Termination of Triangular Integer Loops is Decidable
Alive	AliveInLean: A Verified LLVM Peephole Optimization Verifier
alternating automata	Alternating Automata Modulo First Order Theories
Anonymous Protocols	Probabilistic Bisimulation for Parameterized Systems
approximation	Sound Approximation of Programs with Elementary Functions
architecture	Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors
Artificial Intelligence	Verifai: A Toolkit for the Formal Design and Analysis of Artificial Intelligence-Based Systems
Asynchronous distributed systems	Communication-closed asynchronous protocols
Asynchronous Event-Driven Programs	Verifying Asynchronous Event-Driven Programs Using Partial Abstract Transformers
asynchrony
automata	Synthesizing Approximate Implementations for Unrealizable Specifications Automated Hypersafety Verification
Automated Reasoning	Incremental Determinization for Quantifier Elimination and Functional Synthesis
automated verification	Automated Parameterized Verification of CRDTs Property Directed Self Composition
Autonomous Vehicles	Verifai: A Toolkit for the Formal Design and Analysis of Artificial Intelligence-Based Systems
autonomy	When Human Intuition Fails: Using Formal Methods to Find an Error in the “Proof” of a Multi-Agent Protocol
B
Barrier Certificates	Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems
binary decision diagrams	Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors
biological systems	Semi-Quantitative Abstraction and Analysis of Chemical Reaction Networks
Boolean Algebra Presburger Arithmetic (BAPA)	Verification of Threshold-based Distributed Algorithms by Decomposition to Decidable Logics
boolean closure	Symbolic Register Automata
boolean combination	Multi-Armed Bandits for Boolean Connectives in Hybrid System Falsification
Boolean functional synthesis	Incremental Determinization for Quantifier Elimination and Functional Synthesis
Boolean logic	Incremental Determinization for Quantifier Elimination and Functional Synthesis
Bounded Model Checking	BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings
Bounded Synthesis	Verifying Hyperliveness
buddy memory allocation	Rely-guarantee Reasoning about Concurrent Memory Management in Zephyr RTOS
Büchi emptiness	Robust Controller Synthesis in Timed Büchi Automata: A Symbolic Approach
C
C semantics	Cerberus-BMC: a Principled Reference Semantics and Exploration Tool for Concurrent and Sequential C
C11 concurrency	Cerberus-BMC: a Principled Reference Semantics and Exploration Tool for Concurrent and Sequential C
cache-coherence protocols	Gradual Consistency Checking
CAT	BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings
CEGAR	Abstraction Refinement Algorithms for Timed Automata
CEGIS	Overfitting in Synthesis: Theory and Practice
chemical reaction networks	Semi-Quantitative Abstraction and Analysis of Chemical Reaction Networks
cloud computing	Reachability Analysis for AWS-based Networks
Co-safaty automata	Safety and co-safety comparator automata for discounted-sum inclusion
communicating automata
compiler verification	Icing: Supporting Fast-math Style Optimizations in a Verified Compiler AliveInLean: A Verified LLVM Peephole Optimization Verifier
compositional	Local and Compositional Reasoning For Optimized Reactive Systems
Computational Learning Theory	Efficient Synthesis with Probabilistic Constraints
concurrency	SecCSL: Security Concurrent Separation Logic Automated Hypersafety Verification Violat: Generating Tests of Observational Refinement for Concurrent Objects
concurrent memory management	Rely-guarantee Reasoning about Concurrent Memory Management in Zephyr RTOS
Concurrent Programs	BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings
consistency	Violat: Generating Tests of Observational Refinement for Concurrent Objects
Constrained Horn Clauses	Quantified Invariants via Syntax-Guided-Synthesis
constraint solving	Reachability Analysis for AWS-based Networks
Continuous Systems	Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems
Controller synthesis	Robust Controller Synthesis in Timed Büchi Automata: A Symbolic Approach Flexible Computational Pipelines for Robust Abstraction-based Control Synthesis
counterexample-guided abstraction refinement	Efficient verification of network fault tolerance via counterexample-guided refinement
counterexample-guided inductive synthesis	Overfitting in Synthesis: Theory and Practice
Cyber-physical systems	Multi-Armed Bandits for Boolean Connectives in Hybrid System Falsification StreamLAB: Stream-based Monitoring of Cyber-Physical Systems Verifai: A Toolkit for the Formal Design and Analysis of Artificial Intelligence-Based Systems
D
decidability	Termination of Triangular Integer Loops is Decidable
decidable logic	Inferring Inductive Invariants from Phase Structures
Deductive verification	Verification of Threshold-based Distributed Algorithms by Decomposition to Decidable Logics Communication-closed asynchronous protocols
Delay Differential Equations (DDEs)	Taming Delays in Dynamical Systems: Unbounded Verification of Delay Differential Equations
Diagonal constraints	Fast algorithms for handling diagonal constraints in timed automata
Discounted-sum comparator	Safety and co-safety comparator automata for discounted-sum inclusion
Discounted-sum inclusion	Safety and co-safety comparator automata for discounted-sum inclusion
Distibuted protocols	Verification of Threshold-based Distributed Algorithms by Decomposition to Decidable Logics
distributed protocols	Inferring Inductive Invariants from Phase Structures
Distributed Systems	Checking Robustness Against Snapshot Isolation When Human Intuition Fails: Using Formal Methods to Find an Error in the “Proof” of a Multi-Agent Protocol
E
Effectively proposition logic (EPR)	Verification of Threshold-based Distributed Algorithms by Decomposition to Decidable Logics
elementary functions	Sound Approximation of Programs with Elementary Functions
enumerative algorithm	Abstraction Refinement Algorithms for Timed Automata
F
falsification	Multi-Armed Bandits for Boolean Connectives in Hybrid System Falsification Verifai: A Toolkit for the Formal Design and Analysis of Artificial Intelligence-Based Systems
fault tolerance analysis	Efficient verification of network fault tolerance via counterexample-guided refinement
Finite Abstraction	Flexible Computational Pipelines for Robust Abstraction-based Control Synthesis
first order logic	Alternating Automata Modulo First Order Theories
fixed size bit-vectors	Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors
floating-point arithmetic	Icing: Supporting Fast-math Style Optimizations in a Verified Compiler Sound Approximation of Programs with Elementary Functions
Floating-Points	Invertibility Conditions for Floating-Point Formulas
Formal methods	Integrating Formal Schedulability Analysis into a Verifed OS Kernel Verifai: A Toolkit for the Formal Design and Analysis of Artificial Intelligence-Based Systems
Formal verification	Formal verification of quantum algorithms using quantum Hoare logic
Forward analysis	Fast algorithms for handling diagonal constraints in timed automata
Functional Reactive Programming	Temporal Stream Logic: Synthesis beyond the Bools
G
games	PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games
H
HyperLTL	Verifying Hyperliveness
Hyperproperties	Verifying Hyperliveness
hypersafety	Automated Hypersafety Verification
I
implemetation	Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors
Inductive Invariants	Interpolating Strong Induction Quantified Invariants via Syntax-Guided-Synthesis
Inductive Proofs	Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems
infinite alphabets	Alternating Automata Modulo First Order Theories
infinite state	Local and Compositional Reasoning For Optimized Reactive Systems
Infinite State Symbolic Model Checking	Extending nuXmv with Timed Transition Systems and Timed Temporal Properties
infinite-domain data	Symbolic Monitoring against Specifications Parametric in Time and Data
infinite-state	STAMINA: STochastic Approximate Model-checker for INfinite-state Analysis
Information Flow Control	SecCSL: Security Concurrent Separation Logic
integer programs	Termination of Triangular Integer Loops is Decidable
Interpolation	Interpolating Strong Induction Alternating Automata Modulo First Order Theories
Invariant generation	Loop Summarization with Rational Vector Addition Systems
invariant inference	Inferring Inductive Invariants from Phase Structures
Invertibility Conditions	Invertibility Conditions for Floating-Point Formulas
Isabelle/HOL	Formal verification of quantum algorithms using quantum Hoare logic Rely-guarantee Reasoning about Concurrent Memory Management in Zephyr RTOS
K
k-induction	Interpolating Strong Induction
k-safety	Property Directed Self Composition
L
language equivalence	Symbolic Register Automata
language inclusion	Symbolic Register Automata
Lean	AliveInLean: A Verified LLVM Peephole Optimization Verifier
Linear hybrid automaton	Membership-based Synthesis of Linear Hybrid Automata
linear loops	Termination of Triangular Integer Loops is Decidable
linearizability	Violat: Generating Tests of Observational Refinement for Concurrent Objects
Linearization	Taming Delays in Dynamical Systems: Unbounded Verification of Delay Differential Equations
LLVM	AliveInLean: A Verified LLVM Peephole Optimization Verifier
local reasoning	Local and Compositional Reasoning For Optimized Reactive Systems
Lyapunov Functions	Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems
M
Machine Learning	Verifai: A Toolkit for the Formal Design and Analysis of Artificial Intelligence-Based Systems The Marabou Framework for Verification and Analysis of Deep Neural Networks
Mapping	Automated Synthesis of Secure Platform Mappings
Markov chains	STAMINA: STochastic Approximate Model-checker for INfinite-state Analysis
Membership	Membership-based Synthesis of Linear Hybrid Automata
memory models	Gradual Consistency Checking
memory object model	Cerberus-BMC: a Principled Reference Semantics and Exploration Tool for Concurrent and Sequential C
message passing concurrency
Metric Temporal Logic	Satisfiability Checking for Mission-Time LTL
Mission-Time LTL	Satisfiability Checking for Mission-Time LTL
model checking	Verifying Hyperliveness Checking Robustness Against Snapshot Isolation Interpolating Strong Induction Satisfiability Checking for Mission-Time LTL Clock Bound Repair for Timed Systems What's wrong with on-the-fly partial order reduction Automated Hypersafety Verification When Human Intuition Fails: Using Formal Methods to Find an Error in the “Proof” of a Multi-Agent Protocol Cerberus-BMC: a Principled Reference Semantics and Exploration Tool for Concurrent and Sequential C
Model Counting	Synthesizing Approximate Implementations for Unrealizable Specifications
monitoring	Symbolic Monitoring against Specifications Parametric in Time and Data
Multi-agent systems	When Human Intuition Fails: Using Formal Methods to Find an Error in the “Proof” of a Multi-Agent Protocol
N
network verification	Efficient verification of network fault tolerance via counterexample-guided refinement
Neural Network Verification	The Marabou Framework for Verification and Analysis of Deep Neural Networks
Nonlinear Systems	Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems
notions of correctness	Local and Compositional Reasoning For Optimized Reactive Systems
O
on-the-fly	What's wrong with on-the-fly partial order reduction
operating systems	Rely-guarantee Reasoning about Concurrent Memory Management in Zephyr RTOS
optimization	Icing: Supporting Fast-math Style Optimizations in a Verified Compiler
OS Kernel	Integrating Formal Schedulability Analysis into a Verifed OS Kernel
overfitting	Overfitting in Synthesis: Theory and Practice
P
parameter identification	Symbolic Monitoring against Specifications Parametric in Time and Data
Parameterized Systems	Probabilistic Bisimulation for Parameterized Systems
parametric timed automata	Symbolic Monitoring against Specifications Parametric in Time and Data
parametric timed pattern matching	Symbolic Monitoring against Specifications Parametric in Time and Data
partial order reduction	What's wrong with on-the-fly partial order reduction
Peephole Optimization	AliveInLean: A Verified LLVM Peephole Optimization Verifier
performance	Sound Approximation of Programs with Elementary Functions
Platform	Automated Synthesis of Secure Platform Mappings
Probabilistic Bisimulation	Probabilistic Bisimulation for Parameterized Systems
Probabilistic Programs	Efficient Synthesis with Probabilistic Constraints
Probabilistic simulation	Security-Aware Synthesis Using Delayed-Action Games
probabilistic verification	Semi-Quantitative Abstraction and Analysis of Chemical Reaction Networks PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games
Program Reachability	Proving Unrealizability for Syntax-Guided Synthesis
Program Synthesis	Efficient Synthesis with Probabilistic Constraints Proving Unrealizability for Syntax-Guided Synthesis
Program Verification	Quantified Invariants via Syntax-Guided-Synthesis SecCSL: Security Concurrent Separation Logic
Proof Assistant	Integrating Formal Schedulability Analysis into a Verifed OS Kernel
Property Directed	Property Directed Self Composition
Property Directed Reachability	Interpolating Strong Induction
Protocol	Automated Synthesis of Secure Platform Mappings
Q
QBF	Synthesizing Approximate Implementations for Unrealizable Specifications Incremental Determinization for Quantifier Elimination and Functional Synthesis
Quantified Boolean Formulas	Incremental Determinization for Quantifier Elimination and Functional Synthesis
Quantifier Elimination	Incremental Determinization for Quantifier Elimination and Functional Synthesis
Quantifiers	Invertibility Conditions for Floating-Point Formulas Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors
Quantitaive inclusion	Safety and co-safety comparator automata for discounted-sum inclusion
Quantitative games	Run-Time Optimization for Learned Controllers through Quantitative Games
Quantitative Information Flow	Quantitative Mitigation of Timing Side Channels
Quantitative verification	Safety and co-safety comparator automata for discounted-sum inclusion
Quantum computing	Formal verification of quantum algorithms using quantum Hoare logic
Queue invariant	Verifying Asynchronous Event-Driven Programs Using Partial Abstract Transformers
R
Reachability	Fast algorithms for handling diagonal constraints in timed automata
reachability analysis	Reachability Analysis for AWS-based Networks
Reactive Systems	Local and Compositional Reasoning For Optimized Reactive Systems Temporal Stream Logic: Synthesis beyond the Bools
Real-time Properties	StreamLAB: Stream-based Monitoring of Cyber-Physical Systems
Real-Time Scheduling	Integrating Formal Schedulability Analysis into a Verifed OS Kernel
Reduction Proof	Proving Unrealizability for Syntax-Guided Synthesis
Reduction techniques	Communication-closed asynchronous protocols
refinement	Automated Hypersafety Verification
refinement map	Local and Compositional Reasoning For Optimized Reactive Systems
register automata	Symbolic Register Automata
Reinforcement learning	Run-Time Optimization for Learned Controllers through Quantitative Games
Relational Interfaces	Flexible Computational Pipelines for Robust Abstraction-based Control Synthesis
relaxed memory model	Cerberus-BMC: a Principled Reference Semantics and Exploration Tool for Concurrent and Sequential C
rely-guarantee reasoning	Rely-guarantee Reasoning about Concurrent Memory Management in Zephyr RTOS
repair	Clock Bound Repair for Timed Systems
replicated data types	On the Complexity of Checking Consistency for Replicated Data Types
Replicated Systems	Automated Parameterized Verification of CRDTs
Rewriting	High-Level Abstractions for Simplifying Extended String Constraints in SMT
Robustness	Robust Controller Synthesis in Timed Büchi Automata: A Symbolic Approach
Runtime Verification	Symbolic Monitoring against Specifications Parametric in Time and Data StreamLAB: Stream-based Monitoring of Cyber-Physical Systems
S
Safety	Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems
Safety and stability	Taming Delays in Dynamical Systems: Unbounded Verification of Delay Differential Equations
Safety automata	Safety and co-safety comparator automata for discounted-sum inclusion
SAT	Incremental Determinization for Quantifier Elimination and Functional Synthesis
Satisfiability Checking	Satisfiability Checking for Mission-Time LTL
satisfiability modulo theories	Invertibility Conditions for Floating-Point Formulas Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors
Schedulability Analysis	Integrating Formal Schedulability Analysis into a Verifed OS Kernel
Security	Security-Aware Synthesis Using Delayed-Action Games Automated Synthesis of Secure Platform Mappings
Security Mitigation	Quantitative Mitigation of Timing Side Channels
self composition	Property Directed Self Composition
Separation Logic	SecCSL: Security Concurrent Separation Logic
session types
Shield	Run-Time Optimization for Learned Controllers through Quantitative Games
signal temporal logic	Multi-Armed Bandits for Boolean Connectives in Hybrid System Falsification
Simulation	Verifai: A Toolkit for the Formal Design and Analysis of Artificial Intelligence-Based Systems
Simulations	Fast algorithms for handling diagonal constraints in timed automata
skipping simulation	Local and Compositional Reasoning For Optimized Reactive Systems
SMT	Satisfiability Checking for Mission-Time LTL High-Level Abstractions for Simplifying Extended String Constraints in SMT Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings CVC4SY: Smart and Fast Term Enumeration for Syntax-Guided Synthesis The Marabou Framework for Verification and Analysis of Deep Neural Networks
SMT solving	Clock Bound Repair for Timed Systems
SMT-based model checking	Property Directed Self Composition
Snapshot Isolation	Checking Robustness Against Snapshot Isolation
Spectral analysis	Taming Delays in Dynamical Systems: Unbounded Verification of Delay Differential Equations
Spin	What's wrong with on-the-fly partial order reduction
Stability	Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems
statistical model checking	PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games
stepwise refinement	Local and Compositional Reasoning For Optimized Reactive Systems
Stochastic games	Security-Aware Synthesis Using Delayed-Action Games
Stochastic model checking	STAMINA: STochastic Approximate Model-checker for INfinite-state Analysis
stochastic processes	PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games
stochastic systems	Semi-Quantitative Abstraction and Analysis of Chemical Reaction Networks
Strategies	Verifying Hyperliveness
Strategy synthesis	Security-Aware Synthesis Using Delayed-Action Games
Stream-based Monitoring	StreamLAB: Stream-based Monitoring of Cyber-Physical Systems
Strings	High-Level Abstractions for Simplifying Extended String Constraints in SMT
stuttering simulation	Local and Compositional Reasoning For Optimized Reactive Systems
SyGuS	Overfitting in Synthesis: Theory and Practice
Symbolic algorithm	Abstraction Refinement Algorithms for Timed Automata Robust Controller Synthesis in Timed Büchi Automata: A Symbolic Approach
symbolic automata	Symbolic Register Automata
Symbolic Timed Transition Systems	Extending nuXmv with Timed Transition Systems and Timed Temporal Properties
Synchronous distributed systems	Communication-closed asynchronous protocols
syntax-guided synthesis	Overfitting in Synthesis: Theory and Practice CVC4SY: Smart and Fast Term Enumeration for Syntax-Guided Synthesis
Synthesis	Synthesizing Approximate Implementations for Unrealizable Specifications Temporal Stream Logic: Synthesis beyond the Bools Membership-based Synthesis of Linear Hybrid Automata Run-Time Optimization for Learned Controllers through Quantitative Games Automated Synthesis of Secure Platform Mappings Incremental Determinization for Quantifier Elimination and Functional Synthesis
T
Temporal Logics	Temporal Stream Logic: Synthesis beyond the Bools
Term Enumeration	CVC4SY: Smart and Fast Term Enumeration for Syntax-Guided Synthesis
termination	Termination of Triangular Integer Loops is Decidable
testing	Gradual Consistency Checking On the Complexity of Checking Consistency for Replicated Data Types Violat: Generating Tests of Observational Refinement for Concurrent Objects
timed automata	Abstraction Refinement Algorithms for Timed Automata Robust Controller Synthesis in Timed Büchi Automata: A Symbolic Approach Fast algorithms for handling diagonal constraints in timed automata Clock Bound Repair for Timed Systems Alternating Automata Modulo First Order Theories
Timed Temporal Properties Model Checking	Extending nuXmv with Timed Transition Systems and Timed Temporal Properties
Timed Temporal Properties Validity	Extending nuXmv with Timed Transition Systems and Timed Temporal Properties
Timing Side Channels	Quantitative Mitigation of Timing Side Channels
U
Unbounded message queues	Verifying Asynchronous Event-Driven Programs Using Partial Abstract Transformers
Unbounded verification	Taming Delays in Dynamical Systems: Unbounded Verification of Delay Differential Equations
Unrealizability	Proving Unrealizability for Syntax-Guided Synthesis
user-guided invariant inference	Inferring Inductive Invariants from Phase Structures
V
Vector addition systems	Loop Summarization with Rational Vector Addition Systems
verification	Verifying Asynchronous Event-Driven Programs Using Partial Abstract Transformers Clock Bound Repair for Timed Systems Automated Hypersafety Verification Violat: Generating Tests of Observational Refinement for Concurrent Objects
W
weak consistency	Automated Parameterized Verification of CRDTs On the Complexity of Checking Consistency for Replicated Data Types
Weak Memory Model	BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings
Z
Zones	Fast algorithms for handling diagonal constraints in timed automata

Disclaimer | Powered by EasyChair Smart Program