Revisiting Underapproximate Reachability for Multipushdown Systems . . . . . 387
S. Akshay, Paul Gastin, S Krishna, and Sparsa Roychowdhury
KReach: A Tool for Reachability in Petri Nets . . . . . . . . . . . . . . . . . . . . . . 405
Alex Dixon and Ranko Lazić
AVR: Abstractly Verifying Reachability . . . . . . . . . . . . . . . . . . . . . . . . . . 413
Aman Goel and Karem Sakallah
Timed and Probabilistic Systems
Verified Certification of Reachability Checking for Timed Automata . . . . . . . 425
Simon Wimmer and Joshua von Mutius
Learning One-Clock Timed Automata . . . . . . . . . . . . . . . . . . . . . . . . . . . . 444
Jie An, Mingshuai Chen, Bohua Zhan, Naijun Zhan,
and Miaomiao Zhang
Rare Event Simulation for Non-Markovian Repairable Fault Trees . . . . . . . . 463
Carlos E. Budde, Marco Biagi, Raúl E. Monti, Pedro R. D’Argenio,
and Mariëlle Stoelinga
FIG: The Finite Improbability Generator . . . . . . . . . . . . . . . . . . . . . . . . . . 483
Carlos E. Budde
MORA - Automatic Generation of Moment-Based Invariants . . . . . . . . . . . . . 492
Ezio Bartocci, Laura Kovács, and Miroslav Stankovič
Author Index . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 499
Contents – Part I
xix