ATVA2019: 17TH INTERNATIONAL SYMPOSIUM ON AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS

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

A
abstraction	BUBEN: Automated Library Abstractions Enabling Scalable Bug Detection for Large Programs with I/O and Complex Environment
angelic and demonic nondeterminism	Deciding Fast Termination for Probabilistic VASS with Nondeterminism
Approximation	Synthesizing Efficient Low-Precision Kernels
Asynchronous Systems	Efficient Trace Encodings of Bounded Synthesis for Asynchronous Distributed Systems
automata	New Optimizations and Heuristics for Determinization of Büchi Automata
automata over infinite alphabets	DEQ : Equivalence Checker for Deterministic Register Automata
Automate over infinite words	Approximate Automata for Omega-regular Languages
B
Bounded Synthesis	Efficient Trace Encodings of Bounded Synthesis for Asynchronous Distributed Systems
Büchi	New Optimizations and Heuristics for Determinization of Büchi Automata
C
Causality Checking	An Efficient Algorithm for Computing Causal Trace Sets in Causality Checking
Circuits	Model Checking Data Flows in Concurrent Network Updates
combination approach	Conditional Testing: Off-the-Shelf Combination of Test-Case Generators
Complexity	Program Repair for Hyperproperties [Best Paper Award Candidate]
computational group theory	DEQ : Equivalence Checker for Deterministic Register Automata
Concolic execution	KLUZZER: Whitebox Fuzzing on top of LLVM
cooperative verification	Conditional Testing: Off-the-Shelf Combination of Test-Case Generators
D
Data Flow	Model Checking Data Flows in Concurrent Network Updates
data parallelism	Adaptive Online First-Order Monitoring
data structures	Enhancing Symbolic Execution of Heap-based Programs with Separation Logic for Test Input Generation
deterministic	LTL3TELA: Small Deterministic or Nondeterministic Automata from LTL
determinization	New Optimizations and Heuristics for Determinization of Büchi Automata
Distributed Systems	Efficient Trace Encodings of Bounded Synthesis for Asynchronous Distributed Systems
dynamic analysis	BUBEN: Automated Library Abstractions Enabling Scalable Bug Detection for Large Programs with I/O and Complex Environment
E
Elementary Functions	Synthesizing Efficient Low-Precision Kernels
Emerson-Lei automata	Generic Emptiness Check for Fun and Profit LTL3TELA: Small Deterministic or Nondeterministic Automata from LTL
emptiness check	Generic Emptiness Check for Fun and Profit
equivariant dynamical systems	Using Symmetry Transformations in Equivariant Dynamical Systems for their Safety Verification [Best Paper Award Candidate]
F
Fault Tree	An Efficient Algorithm for Computing Causal Trace Sets in Causality Checking
Finite Precision	Synthesizing Efficient Low-Precision Kernels
G
Game	Teaching Stratego to Play Ball : Optimal Synthesis for Continuous Space MDPs
games	Semantic Labelling and Learning for Parity Game Solving in LTL Synthesis [Best Paper Award Candidate]
graphical user interfaces	Reactive Synthesis of Graphical User Interface Glue Code
H
heap-based programs	Enhancing Symbolic Execution of Heap-based Programs with Separation Logic for Test Input Generation
heuristics	New Optimizations and Heuristics for Determinization of Büchi Automata
Higher-order moments	Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops
Hyperproperties	Program Repair for Hyperproperties [Best Paper Award Candidate]
I
IMITATOR	Parametric Timed Model Checking for Guaranteeing Timed Opacity
Information Flow	Efficient Information-Flow Verification under Speculative Execution
Information flow security	Program Repair for Hyperproperties [Best Paper Award Candidate]
L
lazy initialization	Enhancing Symbolic Execution of Heap-based Programs with Separation Logic for Test Input Generation
Lerning	Teaching Stratego to Play Ball : Optimal Synthesis for Continuous Space MDPs
linear temporal logic	Semantic Labelling and Learning for Parity Game Solving in LTL Synthesis [Best Paper Award Candidate]
Linear-time properties	Approximate Automata for Omega-regular Languages
LLVM	KLUZZER: Whitebox Fuzzing on top of LLVM
LTL	LTL3TELA: Small Deterministic or Nondeterministic Automata from LTL
LTL3TELA	LTL3TELA: Small Deterministic or Nondeterministic Automata from LTL
M
Markov Chains	Are Parametric Markov Chains Monotonic?
Markov decision process	Generic Emptiness Check for Fun and Profit
MDP	Teaching Stratego to Play Ball : Optimal Synthesis for Continuous Space MDPs
Minimal Counterexamples	An Efficient Algorithm for Computing Causal Trace Sets in Causality Checking
Minimal Traces	An Efficient Algorithm for Computing Causal Trace Sets in Causality Checking
Model Checking	Generic Emptiness Check for Fun and Profit An Efficient Algorithm for Computing Causal Trace Sets in Causality Checking Model Checking Data Flows in Concurrent Network Updates
Model-based Design	Performance Evaluation of NDN Data Plane Using Statistical Model Checking
monitoring	Multi-Head Monitoring of Metric Temporal Logic Adaptive Online First-Order Monitoring
Monotonicity	Are Parametric Markov Chains Monotonic?
N
NDN	Performance Evaluation of NDN Data Plane Using Statistical Model Checking
Netweorking	Performance Evaluation of NDN Data Plane Using Statistical Model Checking
nominal sets	DEQ : Equivalence Checker for Deterministic Register Automata
O
omega-automata	LTL3TELA: Small Deterministic or Nondeterministic Automata from LTL Reactive Synthesis of Graphical User Interface Glue Code
opacity	Parametric Timed Model Checking for Guaranteeing Timed Opacity
Optimization	Teaching Stratego to Play Ball : Optimal Synthesis for Continuous Space MDPs
optimizations	New Optimizations and Heuristics for Determinization of Büchi Automata
P
parameter synthesis	Are Parametric Markov Chains Monotonic? Parametric Timed Model Checking for Guaranteeing Timed Opacity
parity	New Optimizations and Heuristics for Determinization of Büchi Automata
Petri Games	Efficient Trace Encodings of Bounded Synthesis for Asynchronous Distributed Systems
Petri Nets	Model Checking Data Flows in Concurrent Network Updates
Probabilistic Invariants	Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops
Probabilistic Model Checking	Are Parametric Markov Chains Monotonic?
Probabilistic Programs	Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops
probabilistic VASS	Deciding Fast Termination for Probabilistic VASS with Nondeterminism
Program Analysis	Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops
Program verification	Chain Free String Constraints [Best Paper Award Candidate]
R
reactive synthesis	Reactive Synthesis of Graphical User Interface Glue Code
Refinement	Teaching Stratego to Play Ball : Optimal Synthesis for Continuous Space MDPs
register automata	DEQ : Equivalence Checker for Deterministic Register Automata
reinforcement learning	Semantic Labelling and Learning for Parity Game Solving in LTL Synthesis [Best Paper Award Candidate]
Repair	Program Repair for Hyperproperties [Best Paper Award Candidate]
Runtime Verification	Multi-Head Monitoring of Metric Temporal Logic Adaptive Online First-Order Monitoring
S
safety verification	Using Symmetry Transformations in Equivariant Dynamical Systems for their Safety Verification [Best Paper Award Candidate]
Satisfiability modulo theories	Chain Free String Constraints [Best Paper Award Candidate]
sensitivity analysis	Using Symmetry Transformations in Equivariant Dynamical Systems for their Safety Verification [Best Paper Award Candidate]
separation logic	Enhancing Symbolic Execution of Heap-based Programs with Separation Logic for Test Input Generation
Side-Channels	Efficient Information-Flow Verification under Speculative Execution
SMC	Performance Evaluation of NDN Data Plane Using Statistical Model Checking
Software Defined Networks	Model Checking Data Flows in Concurrent Network Updates
Software testing	KLUZZER: Whitebox Fuzzing on top of LLVM Conditional Testing: Off-the-Shelf Combination of Test-Case Generators
Speculative Execution	Efficient Information-Flow Verification under Speculative Execution
state migration	Adaptive Online First-Order Monitoring
State Space Exploration	An Efficient Algorithm for Computing Causal Trace Sets in Causality Checking
state space traversal	BUBEN: Automated Library Abstractions Enabling Scalable Bug Detection for Large Programs with I/O and Complex Environment
static analysis	BUBEN: Automated Library Abstractions Enabling Scalable Bug Detection for Large Programs with I/O and Complex Environment
Stratego	Teaching Stratego to Play Ball : Optimal Synthesis for Continuous Space MDPs
String constraint solving	Chain Free String Constraints [Best Paper Award Candidate]
symbolic execution	Enhancing Symbolic Execution of Heap-based Programs with Separation Logic for Test Input Generation
symmetry	Using Symmetry Transformations in Equivariant Dynamical Systems for their Safety Verification [Best Paper Award Candidate]
Synthesis	Approximate Automata for Omega-regular Languages Semantic Labelling and Learning for Parity Game Solving in LTL Synthesis [Best Paper Award Candidate] Program Repair for Hyperproperties [Best Paper Award Candidate] Synthesizing Efficient Low-Precision Kernels
T
TELA	LTL3TELA: Small Deterministic or Nondeterministic Automata from LTL
Temporal Logic	Model Checking Data Flows in Concurrent Network Updates Multi-Head Monitoring of Metric Temporal Logic Adaptive Online First-Order Monitoring
termination time	Deciding Fast Termination for Probabilistic VASS with Nondeterminism
test input generation	Enhancing Symbolic Execution of Heap-based Programs with Separation Logic for Test Input Generation
test-case generation	Conditional Testing: Off-the-Shelf Combination of Test-Case Generators
timed automata	Parametric Timed Model Checking for Guaranteeing Timed Opacity
Trace-length independence	Multi-Head Monitoring of Metric Temporal Logic
U
Uppaal	Teaching Stratego to Play Ball : Optimal Synthesis for Continuous Space MDPs
V
Verification	Efficient Information-Flow Verification under Speculative Execution Approximate Automata for Omega-regular Languages
W
Whitebox fuzzing	KLUZZER: Whitebox Fuzzing on top of LLVM
ω
ω-automata	Generic Emptiness Check for Fun and Profit

Disclaimer | Powered by EasyChair Smart Program