Tools and Algorithms for the Construction and Analysis of Systems: 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6–11, 2019, Proceedings, Part II

Front Matter ....Pages i-xxiii
Front Matter ....Pages 1-1
 Checking Deadlock-Freedom of Parametric Component-Based Systems  (Marius Bozga, Radu Iosif, Joseph Sifakis)....Pages 3-20
 The mCRL2 Toolset for Analysing Concurrent Systems  (Olav Bunte, Jan Friso Groote, Jeroen J. A. Keiren, Maurice Laveaux, Thomas Neele, Erik P. de Vink et al.)....Pages 21-39
 Automatic Analysis of Consistency Properties of Distributed Transaction Systems in Maude  (Si Liu, Peter Csaba Ölveczky, Min Zhang, Qi Wang, José Meseguer)....Pages 40-57
 Multi-core On-The-Fly Saturation  (Tom van Dijk, Jeroen Meijer, Jaco van de Pol)....Pages 58-75
Front Matter ....Pages 77-77
 Specification and Efficient Monitoring Beyond STL  (Alexey Bakhirkin, Nicolas Basset)....Pages 79-97
 VyPR2: A Framework for Runtime Verification of Python Web Services  (Joshua Heneage Dawes, Giles Reger, Giovanni Franzoni, Andreas Pfeiffer, Giacomo Govi)....Pages 98-114
 Constraint-Based Monitoring of Hyperproperties  (Christopher Hahn, Marvin Stenger, Leander Tentrup)....Pages 115-131
Front Matter ....Pages 133-133
 Tail Probabilities for Randomized Program Runtimes via Martingales for Higher Moments  (Satoshi Kura, Natsuki Urabe, Ichiro Hasuo)....Pages 135-153
 Computing the Expected Execution Time of Probabilistic Workflow Nets  (Philipp J. Meyer, Javier Esparza, Philip Offtermatt)....Pages 154-171
 Shepherding Hordes of Markov Chains  (Milan Češka, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen)....Pages 172-190
 Optimal Time-Bounded Reachability Analysis for Concurrent Systems  (Yuliya Butkova, Gereon Fox)....Pages 191-208
Front Matter ....Pages 209-209
 Minimal-Time Synthesis for Parametric Timed Automata  (Étienne André, Vincent Bloemen, Laure Petrucci, Jaco van de Pol)....Pages 211-228
 Environmentally-Friendly GR(1) Synthesis  (Rupak Majumdar, Nir Piterman, Anne-Kathrin Schmuck)....Pages 229-246
 \(\mathsf {StocHy}\): Automated Verification and Synthesis of Stochastic Processes  (Nathalie Cauchi, Alessandro Abate)....Pages 247-264
 Synthesis of Symbolic Controllers: A Parallelized and Sparsity-Aware Approach  (Mahmoud Khaled, Eric S. Kim, Murat Arcak, Majid Zamani)....Pages 265-281
Front Matter ....Pages 283-283
 i\(_\mathrm {Rank}\): A Variable Order Metric for DEDS Subject to Linear Invariants  (Elvio Gilberto Amparore, Gianfranco Ciardo, Susanna Donatelli, Andrew Miner)....Pages 285-302
 Binary Decision Diagrams with Edge-Specified Reductions  (Junaid Babar, Chuan Jiang, Gianfranco Ciardo, Andrew Miner)....Pages 303-318
 Effective Entailment Checking for Separation Logic with Inductive Definitions  (Jens Katelaan, Christoph Matheja, Florian Zuleger)....Pages 319-336
Front Matter ....Pages 337-337
 Digital Bifurcation Analysis of TCP Dynamics  (Nikola Beneš, Luboš Brim, Samuel Pastva, David Šafránek)....Pages 339-356
 Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model Checking  (Ilina Stoilkovska, Igor Konnov, Josef Widder, Florian Zuleger)....Pages 357-374
 Measuring Masking Fault-Tolerance  (Pablo F. Castro, Pedro R. D’Argenio, Ramiro Demasi, Luciano Putruele)....Pages 375-392
 PhASAR: An Inter-procedural Static Analysis Framework for C/C++  (Philipp Dominik Schubert, Ben Hermann, Eric Bodden)....Pages 393-410
Back Matter ....Pages 411-413