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
analytic delay models	A Novel Symbolic Execution Framework for Symbolic Timing Analysis of Digital Integrated Circuits
Arithmetic circuits	Verifying Arithmetic Circuits with Polynomials
automata learning	Leveraging Partial Redundancy in Active Automata Learning 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
Constrained Horn Clauses	CHCs for every occasion
Cooperative Verification	Software Verification Witnesses
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
digital circuit verification	A Novel Symbolic Execution Framework for Symbolic Timing Analysis of Digital Integrated Circuits
E
Elevator automta	Complementing Emerson-Lei Elevator Automata
Exchange Formats	Software Verification Witnesses
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)*
invariants	Bounding Probabilistic Loop Variables using Martingales and the Optional Stopping Theorem
M
martingales	Bounding Probabilistic Loop Variables using Martingales and the Optional Stopping Theorem
mbse	Formal Verification with Configurable Execution Semantics
Mealy Machines	Leveraging Partial Redundancy in Active Automata Learning
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	Leveraging Partial Redundancy in Active Automata Learning
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
optional stopping theorem	Bounding Probabilistic Loop Variables using Martingales and the Optional Stopping Theorem
Owicki–Gries	From Interleavings to Owicki–Gries via Empires: Certificates for Concurrent Program Verification
P
Parameterized Synthesis	Parameterized Infinite-State Reactive Synthesis
parametric timing analysis	A Novel Symbolic Execution Framework for Symbolic Timing Analysis of Digital Integrated Circuits
partial Max-SAT	Robust by Design: SAT-based Automata Learning in the Presence of Noise
probabilistic programs	Bounding Probabilistic Loop Variables using Martingales and the Optional Stopping Theorem
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
Reachability Analysis	CHCs for every occasion
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	Software Verification Witnesses CHCs for every occasion Witness-guided verification in trace abstraction
Software Verification Witnesses	Software Verification Witnesses
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 A Novel Symbolic Execution Framework for Symbolic Timing Analysis of Digital Integrated Circuits
symbolic timing analysis	A Novel Symbolic Execution Framework for Symbolic Timing Analysis of Digital Integrated Circuits
T
Tela	Complementing Emerson-Lei Elevator Automata
Termination	CHCs for every occasion
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