Tools and Algorithms for the Construction and Analysis of Systems

Front Matter ....Pages I-XX
Front Matter ....Pages 1-1
 Computing the Concurrency Threshold of Sound Free-Choice Workflow Nets  (Philipp J. Meyer, Javier Esparza, Hagen Völzer)....Pages 3-19
 Fine-Grained Complexity of Safety Verification  (Peter Chini, Roland Meyer, Prakash Saivasan)....Pages 20-37
 Parameterized Verification of Synchronization in Constrained Reconfigurable Broadcast Networks  (A. R. Balasubramanian, Nathalie Bertrand, Nicolas Markey)....Pages 38-54
 EMME: A Formal Tool for ECMAScript Memory Model Evaluation  (Cristian Mattarei, Clark Barrett, Shu-yu Guo, Bradley Nelson, Ben Smith)....Pages 55-71
Front Matter ....Pages 73-73
 What a Difference a Variable Makes  (Marijn J. H. Heule, Armin Biere)....Pages 75-92
 Abstraction Refinement for Emptiness Checking of Alternating Data Automata  (Radu Iosif, Xiao Xu)....Pages 93-111
 Revisiting Enumerative Instantiation  (Andrew Reynolds, Haniel Barbosa, Pascal Fontaine)....Pages 112-131
 A Non-linear Arithmetic Procedure for Control-Command Software Verification  (Pierre Roux, Mohamed Iguernlala, Sylvain Conchon)....Pages 132-151
Front Matter ....Pages 153-153
 Approximate Reduction of Finite Automata for High-Speed Network Intrusion Detection  (Milan Češka, Vojtěch Havlena, Lukáš Holík, Ondřej Lengál, Tomáš Vojnar)....Pages 155-175
 Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts  (Andreas Katis, Grigory Fedyukovich, Huajun Guo, Andrew Gacek, John Backes, Arie Gurfinkel et al.)....Pages 176-193
 \(\text {RVHyper}\): A Runtime Verification Tool for Temporal Hyperproperties  (Bernd Finkbeiner, Christopher Hahn, Marvin Stenger, Leander Tentrup)....Pages 194-200
 The Refinement Calculus of Reactive Systems Toolset  (Iulia Dragomir, Viorel Preoteasa, Stavros Tripakis)....Pages 201-208
Front Matter ....Pages 209-209
 TESTOR: A Modular Tool for On-the-Fly Conformance Test Case Generation  (Lina Marsso, Radu Mateescu, Wendelin Serwe)....Pages 211-228
 Optimal Dynamic Partial Order Reduction with Observers  (Stavros Aronis, Bengt Jonsson, Magnus Lång, Konstantinos Sagonas)....Pages 229-248
 Structurally Defined Conditional Data-Flow Static Analysis  (Elena Sherman, Matthew B. Dwyer)....Pages 249-265
 Geometric Nontermination Arguments  (Jan Leike, Matthias Heizmann)....Pages 266-283
Front Matter ....Pages 285-285
 Efficient Dynamic Error Reduction for Hybrid Systems Reachability Analysis  (Stefan Schupp, Erika Ábrahám)....Pages 287-302
 AMT 2.0: Qualitative and Quantitative Trace Analysis with Extended Signal Temporal Logic  (Dejan Ničković, Olivier Lebeltel, Oded Maler, Thomas Ferrère, Dogan Ulus)....Pages 303-319
 Multi-cost Bounded Reachability in MDP  (Arnd Hartmanns, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann)....Pages 320-339
 A Statistical Model Checker for Nondeterminism and Rare Events  (Carlos E. Budde, Pedro R. D’Argenio, Arnd Hartmanns, Sean Sedwards)....Pages 340-358
Front Matter ....Pages 359-359
 Permutation Games for the Weakly Aconjunctive \(\mu \)-Calculus  (Daniel Hausmann, Lutz Schröder, Hans-Peter Deifel)....Pages 361-378
 Symmetry Reduction for the Local Mu-Calculus  (Kedar S. Namjoshi, Richard J. Trefler)....Pages 379-395
 Bayesian Statistical Parameter Synthesis for Linear Temporal Properties of Stochastic Models  (Luca Bortolussi, Simone Silvetti)....Pages 396-413
Front Matter ....Pages 415-415
 2LS: Memory Safety and Non-termination  (Viktor Malík, Štefan Martiček, Peter Schrammel, Mandayam Srivas, Tomáš Vojnar, Johanan Wahlang)....Pages 417-421
 YOGAR-CBMC: CBMC with Scheduling Constraint Based Abstraction Refinement  (Liangze Yin, Wei Dong, Wanwei Liu, Yunchou Li, Ji Wang)....Pages 422-426
 CPA-BAM-Slicing: Block-Abstraction Memoization and Slicing with Region-Based Dependency Analysis  (Pavel Andrianov, Vadim Mutilin, Mikhail Mandrykin, Anton Vasilyev)....Pages 427-431
 InterpChecker: Reducing State Space via Interpolations  (Zhao Duan, Cong Tian, Zhenhua Duan, C.-H. Luke Ong)....Pages 432-436
 Map2Check Using LLVM and KLEE  (Rafael Menezes, Herbert Rocha, Lucas Cordeiro, Raimundo Barreto)....Pages 437-441
 Symbiotic 5: Boosted Instrumentation  (Marek Chalupa, Martina Vitovská, Jan Strejček)....Pages 442-446
 Ultimate Automizer and the Search for Perfect Interpolants  (Matthias Heizmann, Yu-Fang Chen, Daniel Dietsch, Marius Greitschus, Jochen Hoenicke, Yong Li et al.)....Pages 447-451
 Ultimate Taipan with Dynamic Block Encoding  (Daniel Dietsch, Marius Greitschus, Matthias Heizmann, Jochen Hoenicke, Alexander Nutz, Andreas Podelski et al.)....Pages 452-456
 VeriAbs: Verification by Abstraction and Test Generation  (Priyanka Darke, Sumanth Prabhu, Bharti Chimdyalwar, Avriti Chauhan, Shrawan Kumar, Animesh Basakchowdhury et al.)....Pages 457-462
Back Matter ....Pages 463-465