ATVA 2024: 22ND INTERNATIONAL SYMPOSIUM ON AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS

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

\
\omega-regular objectives	Games with Weighted Multiple Objectives
A
abstraction refinement	Policies Grow on Trees: Model Checking Families of MDPs (**Distinguished Paper**)
Active learning	Greybox Learning of Languages Recognizable by Event-Recording Automata
Advice automata	Query Learning Bounds for Advice and Nominal Automata
Asynchronous Automata	Distribution of Reconfiguration Languages maintaining Tree-like Communication Topology
Automata Learning	Learning Broadcast Protocols with LeoParDS (TOOL Paper) Greybox Learning of Languages Recognizable by Event-Recording Automata
Automata on infinite words	Easy Complementation of History-Deterministic B\"uchi Automata
axiomatic memory consistency model	Formalisation of a new weak Semantics for AuDaLa
B
Binary decision diagram	Symbolic Model Checking of Hybrid CTL on Coloured Kripke Structures
Boolean abstraction	Predictable and Performant Reactive Synthesis Modulo Theories via Functional Synthesis
Boolean networks	Symbolic Model Checking of Hybrid CTL on Coloured Kripke Structures
broadcast protocols	Learning Broadcast Protocols with LeoParDS (TOOL Paper)
Büchi games	A Decremental Algorithm for Fair Büchi Games (**Distinguished Paper**)
C
certification	WhyMon: A Runtime Monitoring Tool with Explanations as Verdicts (TOOL paper)
characteristic samples	Learning Broadcast Protocols with LeoParDS (TOOL Paper)
Coloured Kripke structures	Symbolic Model Checking of Hybrid CTL on Coloured Kripke Structures
Complementation	Easy Complementation of History-Deterministic B\"uchi Automata
completeness	CTL* Verification and Synthesis using Existential Horn Clauses
concurrent systems	Learning Broadcast Protocols with LeoParDS (TOOL Paper)
configurable systems	Configuration Monitor Synthesis
cooperative verification	CPA-Daemon: Mitigating Tool Restarts for Java-Based Verifiers (TOOL paper)
CTL* synthesis	CTL* Verification and Synthesis using Existential Horn Clauses
CTL* verification	CTL* Verification and Synthesis using Existential Horn Clauses
Cutoffs	Proving Cutoff Bounds for Safety Properties in First-Order Logic
Cyber-Physical Systems	Fast Koopman Surrogate Falsification using Linear Relaxations and Weights Deep-Reinforcement-Learning-Based Design Space Exploration for Time-Sensitive Networking
D
decremental algorithms	A Decremental Algorithm for Fair Büchi Games (**Distinguished Paper**)
Deductive Verification	Proving Cutoff Bounds for Safety Properties in First-Order Logic
Deep Reinforcement Learning	Deep-Reinforcement-Learning-Based Design Space Exploration for Time-Sensitive Networking
Determinization	Easy Complementation of History-Deterministic B\"uchi Automata
diagnosis	Configuration Monitor Synthesis
Distributed Systems	Distribution of Reconfiguration Languages maintaining Tree-like Communication Topology
dynamic algorithms	A Decremental Algorithm for Fair Büchi Games (**Distinguished Paper**)
E
Event-recording automata	Greybox Learning of Languages Recognizable by Event-Recording Automata
Existential Horn Clauses	CTL* Verification and Synthesis using Existential Horn Clauses
explanations	WhyMon: A Runtime Monitoring Tool with Explanations as Verdicts (TOOL paper)
Expressive reactive systems	Predictable and Performant Reactive Synthesis Modulo Theories via Functional Synthesis
F
fairness	A Decremental Algorithm for Fair Büchi Games (**Distinguished Paper**)
Falsification	Fast Koopman Surrogate Falsification using Linear Relaxations and Weights
First-Order Logic	HyperSAT: Satisfiability of Hyperproperties using First-Order Logic (**Distinguished TOOL Paper**)
First-Order Logic Applications	HyperSAT: Satisfiability of Hyperproperties using First-Order Logic (**Distinguished TOOL Paper**)
First-Order Transition Systems	Proving Cutoff Bounds for Safety Properties in First-Order Logic
formal methods	Configuration Monitor Synthesis
formal verification	WhyMon: A Runtime Monitoring Tool with Explanations as Verdicts (TOOL paper)
Functional Synthesis	Predictable and Performant Reactive Synthesis Modulo Theories via Functional Synthesis
G
Games	Easy Complementation of History-Deterministic B\"uchi Automata
games on graphs	A Decremental Algorithm for Fair Büchi Games (**Distinguished Paper**)
Graph neural network	Guiding Word Equation Solving using Graph Neural Networks
H
hedge automata	Hedge automata revisited: Transforming texts to and from XML
higher-order logics	Higher-Order Fixpoint Logic for Automated Program Verification
History-determinism	Easy Complementation of History-Deterministic B\"uchi Automata
Hybrid CTL	Symbolic Model Checking of Hybrid CTL on Coloured Kripke Structures
HyperLTL	HyperSAT: Satisfiability of Hyperproperties using First-Order Logic (**Distinguished TOOL Paper**)
I
Incremental SMT solving	Structure Mining For Test Case Generation
K
Koopman Operator Linearization	Fast Koopman Surrogate Falsification using Linear Relaxations and Weights
L
learning computational models	Learning Broadcast Protocols with LeoParDS (TOOL Paper)
linear programming relaxation	Fast Koopman Surrogate Falsification using Linear Relaxations and Weights
Local search	Local Search for Checking Satisfiability of Formulas with Trigonometric Functions
LTL modulo theories	Predictable and Performant Reactive Synthesis Modulo Theories via Functional Synthesis
M
Markov decision processes	Policies Grow on Trees: Model Checking Families of MDPs (**Distinguished Paper**)
metric first-order temporal logic	WhyMon: A Runtime Monitoring Tool with Explanations as Verdicts (TOOL paper)
Mixed trigonometric-polynomial	Local Search for Checking Satisfiability of Formulas with Trigonometric Functions
Model checking	Symbolic Model Checking of Hybrid CTL on Coloured Kripke Structures
monitoring	Configuration Monitor Synthesis
N
Nominal automata	Query Learning Bounds for Advice and Nominal Automata
O
operational semantics	Formalisation of a new weak Semantics for AuDaLa
P
parallel programming language	Formalisation of a new weak Semantics for AuDaLa
Parameterized Verification	Learning Broadcast Protocols with LeoParDS (TOOL Paper) Proving Cutoff Bounds for Safety Properties in First-Order Logic
partial order reduction	Dynamic Partial Order Reduction for Transactional Programs on Serializable Platforms
passive learning	Learning Broadcast Protocols with LeoParDS (TOOL Paper)
program verification	Higher-Order Fixpoint Logic for Automated Program Verification
push-down transducers	Hedge automata revisited: Transforming texts to and from XML
Q
Query learning	Query Learning Bounds for Advice and Nominal Automata
R
Reactive synthesis	Predictable and Performant Reactive Synthesis Modulo Theories via Functional Synthesis
Reconfiguration	Distribution of Reconfiguration Languages maintaining Tree-like Communication Topology
robust policies	Policies Grow on Trees: Model Checking Families of MDPs (**Distinguished Paper**)
runtime monitoring	WhyMon: A Runtime Monitoring Tool with Explanations as Verdicts (TOOL paper)
S
Safety Verification	Proving Cutoff Bounds for Safety Properties in First-Order Logic
Satisfiability	HyperSAT: Satisfiability of Hyperproperties using First-Order Logic (**Distinguished TOOL Paper**)
seriializability	Dynamic Partial Order Reduction for Transactional Programs on Serializable Platforms
Signal Temporal Logic	Fast Koopman Surrogate Falsification using Linear Relaxations and Weights
SMT	Local Search for Checking Satisfiability of Formulas with Trigonometric Functions
software engineering	CPA-Daemon: Mitigating Tool Restarts for Java-Based Verifiers (TOOL paper)
software verification	CPA-Daemon: Mitigating Tool Restarts for Java-Based Verifiers (TOOL paper)
soundness	CTL* Verification and Synthesis using Existential Horn Clauses
stochastic games	Policies Grow on Trees: Model Checking Families of MDPs (**Distinguished Paper**)
strategies and memory	Games with Weighted Multiple Objectives
String theory	Guiding Word Equation Solving using Graph Neural Networks
system models	Configuration Monitor Synthesis
T
Test case generation	Structure Mining For Test Case Generation
Time-Sensitive Networking	Deep-Reinforcement-Learning-Based Design Space Exploration for Time-Sensitive Networking
Trace exploration	Structure Mining For Test Case Generation
transactions	Dynamic Partial Order Reduction for Transactional Programs on Serializable Platforms
two-player games	A Decremental Algorithm for Fair Büchi Games (**Distinguished Paper**)
Two-player zero-sum games	Games with Weighted Multiple Objectives
V
validity checking	Higher-Order Fixpoint Logic for Automated Program Verification
W
Weighted games	Games with Weighted Multiple Objectives
Word equation	Guiding Word Equation Solving using Graph Neural Networks
X
XML	Hedge automata revisited: Transforming texts to and from XML
XSD	Hedge automata revisited: Transforming texts to and from XML
XSLT	Hedge automata revisited: Transforming texts to and from XML

Disclaimer | Powered by EasyChair Smart Program