ATVA 2018: INTERNATIONAL SYMPOSIUM ON AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS

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

A
Analysis of Probabilistic Systems	Bisimilarity Distances for Approximate Differential Privacy
arbiter protocols	Information Leakage in Arbiter Protocols
Arrays	Quantifiers on Demand
artificial pancreas falsification	Signal Convolution Logic
automata	Owl: A Library for \omega-Words, Automata, and LTL
autonomous vehicles	A Formally Verified Motion Planners for Autonomous Vehicles
B
Barrier Certificates	Temporal Logic Verification of Stochastic Systems Using Barrier Certificates
Bisimilarity Distances	Bisimilarity Distances for Approximate Differential Privacy
Bisimulation	Bisimilarity Distances for Approximate Differential Privacy
Boogie	Robustness Testing of Intermediate Verifiers
Boolean algebra	Simulation Algorithms for Symbolic Automata
bounded synthesis	Maximum Realizability for Linear Temporal Logic Specifications Bounded Synthesis of Reactive Programs
Brittleness Exposure	Robustness Testing of Intermediate Verifiers
C
Concurrent and multi-agent systems	EVE: A Tool for Temporal Equilibrium Analysis
Concurrent programs	Modular Verification of Concurrent Programs via Sequential Model Checking
Continuous time	Continuous-Time Markov Decisions based on Partial Exploration
control	Round-Bounded Control of Parameterized Systems
Control under delay	What’s to come is still unsure: Synthesizing controllers resilient to delayed interaction
Convex Optimization	Synthesis in pMDPs: A Tale of 1001 Parameters
Convex Polyhedra	Efficient Symbolic Representation of Convex Polyhedra in High-Dimensional Spaces
convolution	Signal Convolution Logic
counter automata	Quadratic Word Equations with Length Constraints, Counter Systems, and Presburger Arithmetic with Divisibility
coverage	Quantitative Projection Coverage for Testing ML-enabled Autonomous Systems
D
decision procedure	Quadratic Word Equations with Length Constraints, Counter Systems, and Presburger Arithmetic with Divisibility
Deep Neural Networks	Neural State Classification for Hybrid Systems
Differential Privacy	Bisimilarity Distances for Approximate Differential Privacy
Discrete-Time Stochastic Systems	Temporal Logic Verification of Stochastic Systems Using Barrier Certificates
E
Efficient algorithmic synthesis	What’s to come is still unsure: Synthesizing controllers resilient to delayed interaction
Ethereum	EthIR: A Framework for High-Level Analysis of Ethereum Bytecode
EVM bytecode	EthIR: A Framework for High-Level Analysis of Ethereum Bytecode
explanation	Optimal Proofs for Linear Temporal Logic on Lasso Words
F
finite-memory automata	Reactive Synthesis of Register Transducers
fixed point	Ranking and Repulsing Supermartingales for Approximating Reachability
Formal Verification	Temporal Logic Verification of Stochastic Systems Using Barrier Certificates
G
games	Round-Bounded Control of Parameterized Systems
GSMPs	SBIP 2.0: Statistical Model Checking Stochastic Real-time Systems
H
Hybrid Systems	Neural State Classification for Hybrid Systems
hyperltl	MGHyper: Checking Satisfiability of HyperLTL formulas beyond the exists-forall Fragment
hyperproperties	MGHyper: Checking Satisfiability of HyperLTL formulas beyond the exists-forall Fragment
I
IC3	Quantifiers on Demand
Infeasibility analysis	Recursive Online Enumeration of All Minimal Unsatisfiable Subsets
infinite words	Owl: A Library for \omega-Words, Automata, and LTL
Intermediate Verification Language	Robustness Testing of Intermediate Verifiers
K
Kantorovich Metric	Bisimilarity Distances for Approximate Differential Privacy
L
Labelled Markov Chains	Bisimilarity Distances for Approximate Differential Privacy
Linear Real Arithmetic	Efficient Symbolic Representation of Convex Polyhedra in High-Dimensional Spaces
linear temporal logic	EVE: A Tool for Temporal Equilibrium Analysis Owl: A Library for \omega-Words, Automata, and LTL A Fragment of Linear Temporal Logic for Universal Very Weak Automata Temporal Logic Verification of Stochastic Systems Using Barrier Certificates A Formally Verified Motion Planners for Autonomous Vehicles Optimal Proofs for Linear Temporal Logic on Lasso Words
LLVM	Verifying Rust Programs with SMACK
LTL	Owl: A Library for \omega-Words, Automata, and LTL
M
manoeuvre automata	A Formally Verified Motion Planners for Autonomous Vehicles
Markov chains	Accelerated Model Checking of Parametric Markov Chains
Markov Decision Process	Continuous-Time Markov Decisions based on Partial Exploration Synthesis in pMDPs: A Tale of 1001 Parameters
martingale	Ranking and Repulsing Supermartingales for Approximating Reachability
maximum realizability	Maximum Realizability for Linear Temporal Logic Specifications
MaxSAT	Maximum Realizability for Linear Temporal Logic Specifications
Minimal unsatisfiable cores	Recursive Online Enumeration of All Minimal Unsatisfiable Subsets
Minimal unsatisfiable subsets	Recursive Online Enumeration of All Minimal Unsatisfiable Subsets
model checking	Accelerated Model Checking of Parametric Markov Chains Modular Verification of Concurrent Programs via Sequential Model Checking A Symbolic Algorithm for Lazy Synthesis of Eager Strategies Synthesis in pMDPs: A Tale of 1001 Parameters Optimal Proofs for Linear Temporal Logic on Lasso Words
model counting	Information Leakage in Arbiter Protocols
modular verification	Modular Verification of Concurrent Programs via Sequential Model Checking
motion planning	A Formally Verified Motion Planners for Autonomous Vehicles
motion primitives	A Formally Verified Motion Planners for Autonomous Vehicles
MTL	SBIP 2.0: Statistical Model Checking Stochastic Real-time Systems
Mutation Testing	Robustness Testing of Intermediate Verifiers
N
Nash equilibria	EVE: A Tool for Temporal Equilibrium Analysis
neural networks and automated driving	Quantitative Projection Coverage for Testing ML-enabled Autonomous Systems
O
omega-automata	A Fragment of Linear Temporal Logic for Universal Very Weak Automata
P
Parameter Synthesis	Synthesis in pMDPs: A Tale of 1001 Parameters
parameterized systems	Round-Bounded Control of Parameterized Systems
Parametric exploration	SBIP 2.0: Statistical Model Checking Stochastic Real-time Systems
parametric models	Accelerated Model Checking of Parametric Markov Chains
Parity games	EVE: A Tool for Temporal Equilibrium Analysis
Partial exploration	Continuous-Time Markov Decisions based on Partial Exploration
path checking	Optimal Proofs for Linear Temporal Logic on Lasso Words
Presburger arithmetic with Divisibility	Quadratic Word Equations with Length Constraints, Counter Systems, and Presburger Arithmetic with Divisibility
probabilistic program	Ranking and Repulsing Supermartingales for Approximating Reachability
probabilistic programming	PSense: Automatic Sensitivity Analysis for Probabilistic Programs
Probabilistic verification	Continuous-Time Markov Decisions based on Partial Exploration
program synthesis	Bounded Synthesis of Reactive Programs
Program Verification	Quantifiers on Demand
proof search	Optimal Proofs for Linear Temporal Logic on Lasso Words
proof system	Optimal Proofs for Linear Temporal Logic on Lasso Words
Q
quantified boolean formulas	MGHyper: Checking Satisfiability of HyperLTL formulas beyond the exists-forall Fragment
Quantified Generalization	Quantifiers on Demand
Quantifiers	Quantifiers on Demand
quantitative information flow	Information Leakage in Arbiter Protocols
R
Rare events	SBIP 2.0: Statistical Model Checking Stochastic Real-time Systems
reachability	Ranking and Repulsing Supermartingales for Approximating Reachability
reachability analysis	A Formally Verified Motion Planners for Autonomous Vehicles
reactive synthesis	Reactive Synthesis of Register Transducers Maximum Realizability for Linear Temporal Logic Specifications
reactive systems	Bounded Synthesis of Reactive Programs
reduction	Simulation Algorithms for Symbolic Automata
register automata	Reactive Synthesis of Register Transducers
register transducers	Reactive Synthesis of Register Transducers
resource analysis	EthIR: A Framework for High-Level Analysis of Ethereum Bytecode
Robustness Testing	Robustness Testing of Intermediate Verifiers
round-bounded verification	Round-Bounded Control of Parameterized Systems
rule-based representation	EthIR: A Framework for High-Level Analysis of Ethereum Bytecode
Rust	Verifying Rust Programs with SMACK
S
safety games	A Symbolic Algorithm for Lazy Synthesis of Eager Strategies What’s to come is still unsure: Synthesizing controllers resilient to delayed interaction
semi-decisionprocedure	MGHyper: Checking Satisfiability of HyperLTL formulas beyond the exists-forall Fragment
sensitivity	PSense: Automatic Sensitivity Analysis for Probabilistic Programs
simulation	Simulation Algorithms for Symbolic Automata
Simulation based reductions	Continuous-Time Markov Decisions based on Partial Exploration
smart contracts	EthIR: A Framework for High-Level Analysis of Ethereum Bytecode
SMT	Verifying Rust Programs with SMACK
Sources of inconsistency	Recursive Online Enumeration of All Minimal Unsatisfiable Subsets
State Classification Problem	Neural State Classification for Hybrid Systems
Statistical analyses	SBIP 2.0: Statistical Model Checking Stochastic Real-time Systems
Statistical Model Checking	SBIP 2.0: Statistical Model Checking Stochastic Real-time Systems
Stochastic systems	SBIP 2.0: Statistical Model Checking Stochastic Real-time Systems
string equations with length constraints	Quadratic Word Equations with Length Constraints, Counter Systems, and Presburger Arithmetic with Divisibility
symbolic analysis	PSense: Automatic Sensitivity Analysis for Probabilistic Programs
symbolic automata	Simulation Algorithms for Symbolic Automata
symbolic execution	Information Leakage in Arbiter Protocols
Symbolic Representation	Efficient Symbolic Representation of Convex Polyhedra in High-Dimensional Spaces
Symbolic State-Space Exploration	Efficient Symbolic Representation of Convex Polyhedra in High-Dimensional Spaces
synthesis	Bounded Synthesis of Reactive Programs A Symbolic Algorithm for Lazy Synthesis of Eager Strategies
Synthesis and verification	EVE: A Tool for Temporal Equilibrium Analysis
T
temporal logic	Maximum Realizability for Linear Temporal Logic Specifications Signal Convolution Logic
Temporal reasoning	EVE: A Tool for Temporal Equilibrium Analysis
testing complex systems	Quantitative Projection Coverage for Testing ML-enabled Autonomous Systems
theorem proving	A Formally Verified Motion Planners for Autonomous Vehicles
Time bounded reachability	Continuous-Time Markov Decisions based on Partial Exploration
Time-Bounded Reachability	Neural State Classification for Hybrid Systems
Tool	SBIP 2.0: Statistical Model Checking Stochastic Real-time Systems Quantitative Projection Coverage for Testing ML-enabled Autonomous Systems
two-way automata	Bounded Synthesis of Reactive Programs
U
universal automata	A Fragment of Linear Temporal Logic for Universal Very Weak Automata
Unsatisfiability analysis	Recursive Online Enumeration of All Minimal Unsatisfiable Subsets
V
Verification	Verifying Rust Programs with SMACK

Disclaimer | Powered by EasyChair Smart Program