AVM25: 17TH ALPINE VERIFICATION MEETING

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

A
abstract interpretation	Computing abstract model-checking transitions using abstract interpretation
algorithm synthesis	Hardware-Optimal Quantum Algorithms
Arithmetic circuits	Verifying Arithmetic Circuits with Polynomials
Automata Learning	Learning Mealy Machines with Sparse Observation Tables Robust by Design: SAT-based Automata Learning in the Presence of Noise
Automata Theory	Towards Minimizing Phase Event Automata
automated reasoning	Arithmetic Solving in Z3
Automated verification	On the Verification of Structured Parameterized Networks
B
back-references	Regexes with Back-References using Register Set Automata
C
certificates	Neural Certificates
Combinatorial solving	Proofs (that contain programs that contain proofs)*
Complementation	Complementing Emerson-Lei Elevator Automata
Computer algebra	Verifying Arithmetic Circuits with Polynomials
Concurrency	RacerF: Lightweight Static Data Race Detection for C Code From Interleavings to Owicki–Gries via Empires: Certificates for Concurrent Program Verification
configurable semantics	Formal Verification with Configurable Execution Semantics
Cooperative Verification	LIV: Loop-Invariant Validation Using Straight-Line Programs
Counting abstraction	On the Verification of Structured Parameterized Networks
D
Data race	RacerF: Lightweight Static Data Race Detection for C Code
dataflow analysis	Computing abstract model-checking transitions using abstract interpretation
Decidability	On the Verification of Structured Parameterized Networks
E
Elevator automta	Complementing Emerson-Lei Elevator Automata
Exchange Formats	LIV: Loop-Invariant Validation Using Straight-Line Programs
explainable AI	Proof-based Space Explanation of Classifying Neural Networks
F
Formal explanation of NNs	Proof-based Space Explanation of Classifying Neural Networks
Formal Requirements Analysis	Towards Minimizing Phase Event Automata
formal verification	Formal Verification with Configurable Execution Semantics
Frama-C	RacerF: Lightweight Static Data Race Detection for C Code
G
Graph grammars	On the Verification of Structured Parameterized Networks
H
Hardware verification	Proofs (that contain programs that contain proofs)*
hardware-aware optimization	Hardware-Optimal Quantum Algorithms
heuristics	On User-defined Decision Guidance in SMT Solvers
I
Infinite-State Systems	Parameterized Infinite-State Reactive Synthesis
Interference-based proofs	Proofs (that contain programs that contain proofs)*
M
mbse	Formal Verification with Configurable Execution Semantics
Mealy Machines	Learning Mealy Machines with Sparse Observation Tables
Minimization	Towards Minimizing Phase Event Automata
model checking	Computing abstract model-checking transitions using abstract interpretation
model inference	Robust by Design: SAT-based Automata Learning in the Presence of Noise
Model Learning	Learning Mealy Machines with Sparse Observation Tables
Multi-terminal binary decision diagrams	Accelerating Decision-diagram-based Quantum Circuit Simulation With Symbolic Execution
N
Neural network classification	Proof-based Space Explanation of Classifying Neural Networks
neural networks	Neural Certificates
non-determinism	Robust by Design: SAT-based Automata Learning in the Presence of Noise
noodlification	Current State of String Solver Z3-Noodler
O
Optimal Classical Planning	Pseudo-Boolean Proof Logging for Optimal Classical Planning
Owicki–Gries	From Interleavings to Owicki–Gries via Empires: Certificates for Concurrent Program Verification
P
Parameterized Synthesis	Parameterized Infinite-State Reactive Synthesis
partial Max-SAT	Robust by Design: SAT-based Automata Learning in the Presence of Noise
probabilistic programs	Positive Almost-Sure Termination of Polynomial Random Walks
Program Analysis	From Interleavings to Owicki–Gries via Empires: Certificates for Concurrent Program Verification
Propositional dynamic logic	Proofs (that contain programs that contain proofs)*
proving	First-Order Proof Checking
Pseudo-Boolean Proof Logging	Pseudo-Boolean Proof Logging for Optimal Classical Planning
Q
quantum computing	Accelerating Decision-diagram-based Quantum Circuit Simulation With Symbolic Execution Hardware-Optimal Quantum Algorithms
R
random walk	Positive Almost-Sure Termination of Polynomial Random Walks
Reactive Synthesis	Parameterized Infinite-State Reactive Synthesis
reasoning	First-Order Proof Checking
regex	Regexes with Back-References using Register Set Automata
register automata	Regexes with Back-References using Register Set Automata
register set automata	Regexes with Back-References using Register Set Automata
S
SAT solving	Proofs (that contain programs that contain proofs)* Robust by Design: SAT-based Automata Learning in the Presence of Noise
Simulation of quantum circuits	Accelerating Decision-diagram-based Quantum Circuit Simulation With Symbolic Execution
SMT	On User-defined Decision Guidance in SMT Solvers Arithmetic Solving in Z3
SMT-LIB	On User-defined Decision Guidance in SMT Solvers
software verification	LIV: Loop-Invariant Validation Using Straight-Line Programs Witness-guided verification in trace abstraction
Software Verification Witnesses	LIV: Loop-Invariant Validation Using Straight-Line Programs
Static Analysis	RacerF: Lightweight Static Data Race Detection for C Code
string solving	Current State of String Solver Z3-Noodler
Symbolic execution	Accelerating Decision-diagram-based Quantum Circuit Simulation With Symbolic Execution
T
Tela	Complementing Emerson-Lei Elevator Automata
termination	Positive Almost-Sure Termination of Polynomial Random Walks
Thread-modular proofs	From Interleavings to Owicki–Gries via Empires: Certificates for Concurrent Program Verification
trace abstraction	Witness-guided verification in trace abstraction
transducers	Current State of String Solver Z3-Noodler
V
verification	From Interleavings to Owicki–Gries via Empires: Certificates for Concurrent Program Verification Verifying Arithmetic Circuits with Polynomials Neural Certificates First-Order Proof Checking Arithmetic Solving in Z3
VeriPB	Pseudo-Boolean Proof Logging for Optimal Classical Planning
W
witnesses	Witness-guided verification in trace abstraction
ω
ω-automata	Complementing Emerson-Lei Elevator Automata

Disclaimer | Powered by EasyChair Smart Program