Tools and Algorithms for the Construction and Analysis of Systems

Description

This book is Open Access under a CC BY licence. The LNCS 10805 and 10806 proceedings set constitutes the proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2018, which took place in Thessaloniki, Greece, in April 2018, held as part of the European Joint Conference on Theory and Practice of Software, ETAPS 2018. The total of 43 full and 11 short papers presented in these volumes was carefully reviewed and selected from 154submissions. The papers are organized in topical sections as follows: Part I: theorem proving; SAT and SMT I; deductive verification; software verification and optimization; model checking; and machine learning. Part II: concurrent and distributed systems; SAT and SMT II; security and reactive systems; static and dynamic program analysis; hybrid and stochastic systems; temporal logic and mu-calculus; 7th Competition on Software Verification – SV-COMP. 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