Tools and Algorithms for the Construction and Analysis of Systems

ion Refinement for Emptiness Checking of Alternating Data Automata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93 Radu Iosif and Xiao Xu Revisiting Enumerative Instantiation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 112 Andrew Reynolds, Haniel Barbosa, and Pascal Fontaine A Non-linear Arithmetic Procedure for Control-Command Software Verification. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 132 Pierre Roux, Mohamed Iguernlala, and Sylvain Conchon Security and Reactive Systems Approximate Reduction of Finite Automata for High-Speed Network Intrusion Detection . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 155 Milan Češka, Vojtěch Havlena, Lukáš Holík, Ondřej Lengál, and Tomáš Vojnar Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 176 Andreas Katis, Grigory Fedyukovich, Huajun Guo, Andrew Gacek, John Backes, Arie Gurfinkel, and Michael W. Whalen RVHyper: A Runtime Verification Tool for Temporal Hyperproperties . . . . . 194 Bernd Finkbeiner, Christopher Hahn, Marvin Stenger, and Leander Tentrup The Refinement Calculus of Reactive Systems Toolset . . . . . . . . . . . . . . . . 201 Iulia Dragomir, Viorel Preoteasa, and Stavros Tripakis Static and Dynamic Program Analysis TESTOR: A Modular Tool for On-the-Fly Conformance Test Case Generation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 211 Lina Marsso, Radu Mateescu, and Wendelin Serwe Optimal Dynamic Partial Order Reduction with Observers . . . . . . . . . . . . . . 229 Stavros Aronis, Bengt Jonsson, Magnus Lång, and Konstantinos Sagonas Structurally Defined Conditional Data-Flow Static Analysis . . . . . . . . . . . . . 249 Elena Sherman and Matthew B. Dwyer Geometric Nontermination Arguments . . . . . . . . . . . . . . . . . . . . . . . . . . . . 266 Jan Leike and Matthias Heizmann Hybrid and Stochastic Systems Efficient Dynamic Error Reduction for Hybrid Systems Reachability Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 287 Stefan Schupp and Erika Ábrahám AMT 2.0: Qualitative and Quantitative Trace Analysis with Extended Signal Temporal Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 303 Dejan Ničković, Olivier Lebeltel, Oded Maler, Thomas Ferrère, and Dogan Ulus Multi-cost Bounded Reachability in MDP . . . . . . . . . . . . . . . . . . . . . . . . . 320 Arnd Hartmanns, Sebastian Junges, Joost-Pieter Katoen, and Tim Quatmann A Statistical Model Checker for Nondeterminism and Rare Events . . . . . . . . 340 Carlos E. Budde, Pedro R. D’Argenio, Arnd Hartmanns, and Sean Sedwards XVI