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

Description

This book is Open Access under a CC BY licence. The LNCS 11427 and 11428 proceedings set constitutes the proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2019, which took place in Prague, Czech Republic, in April 2019, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019. The total of 42 full and 8 short tool demo papers presented in these volumes was carefully reviewed and selected from 164 submissions. The papers are organized in topical sections as follows: Part I: SAT and SMT, SAT solving and theorem proving; verification and analysis; model checking; tool demo; and machine learning. Part II: concurrent and distributed systems; monitoring and runtime verification; hybrid and stochastic systems; synthesis; symbolic verification; and safety and fault-tolerant systems. 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