ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic

TACAS is a forum for researchers, developers and users interested in rigorously based tools and algorithms for the construction and analysis of systems. The conference aims to bridge the gaps between different communities with this common interest and to support them in their quest to improve the utility, reliability, flexibility and efficiency of tools and algorithms for building systems.

Theoretical papers with clear relevance for tool construction and analysis as well as tool descriptions and case studies with a conceptual message are all encouraged. The topics covered by the conference include, but are not limited to:

• specification and verification techniques;
• software and hardware verification;
• analytical techniques for real-time, hybrid, or stochastic systems;
• analytical techniques for safety, security, or dependability;
• SAT and SMT solving;
• theorem-proving;
• model-checking;
• static and dynamic program analysis;
• testing;
• abstraction techniques for modeling and verification;
• compositional and refinement-based methodologies;
• system construction and transformation techniques;
• machine-learning techniques for synthesis and verification;
• tool environments and tool architectures;
• applications and case studies.

## 25 Years of TACAS

This year we celebrate the 25th TACAS anniversary with a special competition event: TOOLympics. In the scope of TOOLympics, we also hold a panel discussion: Moore’s Law, and More?.

Dates
You're viewing the program in a time zone which is different from your device's time zone - change time zone

#### Mon 8 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

 10:30 - 12:30 SAT and SMT ITACAS at SUN I Chair(s): Lijun Zhang Chinese Academy of Sciences 10:3030mTalk Decomposing Farkas InterpolantsTACASMartin Blicha USI Lugano, Switzerland, Antti Hyvärinen , Jan Kofroň Charles University, Natasha Sharygina USI Lugano, Switzerland Link to publication 11:0030mTalk Parallel SAT Simplification on GPU ArchitecturesTACASMuhammad Osama Eindhoven University of Technology, Anton Wijs Eindhoven University of Technology Link to publication 11:3030mTalk Encoding Redundancy for Satisfaction-Driven Clause LearningBest paper nominationTACASMarijn Heule The University of Texas at Austin, Benjamin Kiesl CISPA Helmholtz Center for Information Security, Armin Biere Johannes Kepler University Linz Link to publication 12:0030mTalk WAPS: Weighted and Projected SamplingTACASRahul Gupta , Shubham Sharma , Subhajit Roy IIT Kanpur, India, Kuldeep S. Meel National University of Singapore Link to publication
 14:00 - 16:00 Verification and AnalysisTACAS at SUN I Chair(s): Dirk Beyer LMU Munich 14:0030mTalk LCV: A Verification Tool for Linear Controller SoftwareTACASJunkil Park University of Pennsylvania, Miroslav Pajic Duke University, Oleg Sokolsky University of Pennsylvania, USA, Insup Lee Link to publication 14:3030mTalk Semantic Fault Localization and Suspiciousness RankingTACASMaria Christakis MPI-SWS, Matthias Heizmann University of Freiburg, Muhammad Numair Mansur Max Planck Institute for Software Systems (MPI-SWS), Christian Schilling IST Austria, Valentin Wüstholz ConsenSys Diligence Link to publication 15:0030mTalk Computing Coupled SimilarityTACASBenjamin Bisping Technische Universität Berlin, Uwe Nestmann Link to publication 15:3030mTalk Reachability Analysis for Termination and Confluence of RewritingTACASChristian Sternagel University of Innsbruck, Austria, Akihisa Yamada Link to publication
 16:30 - 18:00 SAT Solving and Theorem ProvingTACAS at SUN I Chair(s): Armin Biere Johannes Kepler University Linz 16:3030mTalk Quantitative Verification of Masked Arithmetic Programs against Side-Channel AttacksTACASPengfei Gao , Hongyi Xie , Jun Zhang , Fu Song , Taolue Chen Birkbeck, University of London Link to publication 17:0030mTalk Incremental Analysis of Evolving Alloy ModelsTACASWenxi Wang The University of Texas at Austin, Texas, USA, Kaiyuan Wang Google, Inc., Milos Gligoric University of Texas at Austin, Sarfraz Khurshid University of Texas at Austin Link to publication 17:3030mTalk Extending a Brainiac Prover to Lambda-Free Higher-Order LogicTACASPetar Vukmirović , Jasmin Blanchette Vrije Universiteit Amsterdam, Simon Cruanes , Stephan Schulz Link to publication

#### Tue 9 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

 10:30 - 12:30 SAT and SMT IITACAS at SUN I Chair(s): Armin Biere Johannes Kepler University Linz 10:3030mTalk Building Better Bit-Blasting for Floating-Point ProblemsBest paper nominationTACASMartin Brain , Florian Schanda Zenuity, Youcheng Sun University of Oxford Link to publication 11:0030mTalk The Axiom Profiler: Understanding and Debugging SMT Quantifier InstantiationsTACASNils Becker , Peter Müller ETH Zurich, Alexander J. Summers ETH Zurich Link to publication 11:3030mTalk On the Empirical Time Complexity of Scale-Free 3-SAT at the Phase TransitionTACAS Link to publication 12:0030mTalk Modular and Efficient Divide-and-Conquer SAT Solver on Top of the Painless FrameworkTACASLudovic Le Frioux , Souheib Baarir , Julien Sopena , Fabrice Kordon Sorbonne University — LIP6 Link to publication
 14:00 - 15:00 Machine LearningTACAS at JUPITER Chair(s): Bernhard Steffen Technical University Dortmund 14:0030mTalk Omega-Regular Objectives in Model-Free Reinforcement LearningTACASErnst Moritz Hahn Queen's University Belfast, Mateo Perez , Sven Schewe University of Liverpool, Fabio Somenzi , Ashutosh Trivedi , Dominik Wojtczak Link to publication 14:3030mTalk Verifiably Safe Off-Model Reinforcement LearningTACASNathan Fulton MIT-IBM Watson AI Lab, André Platzer Carnegie Mellon University Link to publication
 14:00 - 16:00 Tool DemosTACAS at SUN I Chair(s): Marius Mikucionis Aalborg University 14:0015mTalk nonreach – A Tool for Nonreachability AnalysisTACASFlorian Messner , Christian Sternagel University of Innsbruck, Austria Link to publication 14:1515mTalk The Quantitative Verification Benchmark SetTACASArnd Hartmanns University of Twente, Michaela Klauck Saarland Informatics Campus, Saarland University, David Parker University of Birmingham, Tim Quatmann RWTH Aachen University, Enno Ruijters Link to publication 14:3015mTalk ILAng: A Modeling Platform for SoC Verification using Instruction-Level AbstractionsTACASBo-Yuan Huang Princeton University, USA, Hongce Zhang , Aarti Gupta Princeton University, Sharad Malik Princeton University Link to publication 14:4515mTalk MetAcsl: Specification and Verification of High-Level PropertiesTACASVirgile Robles , Nikolai Kosmatov CEA List, Virgile Prevosto CEA Tech List, Pascale Le Gall Link to publication 15:0015mTalk ROLL 1.0: $\omega$-Regular Language Learning LibraryTACASYu-Fang Chen Academia Sinica, Yong Li Institute of Software, Chinese Academy of Sciences, Xuechao Sun , Andrea Turrini State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Junnan Xu Link to publication 15:1515mTalk Symbolic Regex MatcherTACASMargus Veanes Microsoft Research, Olli Saarikivi , Eric Xu Microsoft, USA, Tiki Wan Link to publication 15:3015mTalk COMPASS 3.0TACASMarco Bozzano , Harold Bruintjes , Alessandro Cimatti Fondazione Bruno Kessler, Joost-Pieter Katoen RWTH Aachen University, Thomas Noll RWTH Aachen University, Stefano Tonetta Fondazione Bruno Kessler, Italy Link to publication 15:4515mTalk Debugging of Behavioural Models with CLEARTACASGianluca Barbon Universit� Grenoble Alpes, Inria, LIG, Vincent Leroy University of Grenoble - CNRS, Gwen Salaün University of Grenoble Alpes Link to publication
 16:30 - 18:00 16:3090mDemonstration Interactive session with tools and demos (I)TACAS
 16:30 - 18:00 Model CheckingTACAS at SUN I Chair(s): Florian Zuleger Vienna University of Technology 16:3030mTalk VoxLogicA: a Spatial Model Checker for Declarative Image AnalysisTACASGina Belmonte , Vincenzo Ciancia , Diego Latella , Mieke Massink CNR-ISTI Pisa, Italy Link to publication 17:0030mTalk On Reachability in Parameterized Phaser ProgramsTACAS Link to publication 17:3030mTalk Abstract Dependency Graphs and Their Application to Model CheckingBest paper nominationTACASSøren Enevoldsen , Kim Larsen Aalborg University, Jiri Srba Link to publication

#### Wed 10 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

 10:30 - 12:30 Concurrent and Distributed SystemsTACAS at SUN I Chair(s): Marieke Huisman University of Twente 10:3030mTalk Multi-Core On-The-Fly SaturationTACASTom van Dijk University of Twente, Jeroen Meijer , Jaco van de Pol Aarhus University Link to publication 11:0030mTalk Automatic Analysis of Consistency Properties of Distributed Transaction Systems in MaudeTACASSi Liu , Peter Ölveczky , Min Zhang East China Normal University, Qi Wang , José Meseguer Link to publication 11:3030mTalk The mCRL2 Toolset for Analysing Concurrent Systems: Improvements in Expressivity and UsabilityTACASOlav Bunte , Jan Friso Groote , Jeroen J.A. Keiren , Maurice Laveaux , Thomas Neele , Erik P. de Vink , Wieger Wesselink , Anton Wijs Eindhoven University of Technology, Tim A.C. Willemse Link to publication 12:0030mTalk Checking Deadlock-Freedom of Parametric Component-Based SystemsTACASMarius Bozga Verimag/CNRS, Radu Iosif VERIMAG, CNRS, Université Grenoble-Alpes, Joseph Sifakis Verimag/CNRS Link to publication
 13:00 - 14:00 13:0060mDemonstration Interactive session with tools and demos (II)TACAS
 14:00 - 16:00 Hybrid and Stochastic SystemsTACAS at SUN I Chair(s): Kim Larsen Aalborg University 14:0030mTalk Tail Probabilities for Runtimes of Randomized Programs: Martingale Synthesis for Higher MomentsTACASSatoshi Kura , Natsuki Urabe , Ichiro Hasuo National Institute of Informatics Link to publication 14:3030mTalk Computing the Expected Execution Time of Probabilistic Workflow NetsTACAS Link to publication 15:0030mTalk Shepherding Hordes of Markov ChainsTACASMilan Ceska Brno University of Technology , Nils Jansen RWTH Aachen University, Sebastian Junges RWTH Aachen University, Germany, Joost-Pieter Katoen RWTH Aachen University Link to publication 15:3030mTalk Optimal Time-Bounded Reachability Analysis for Concurrent SystemsTACAS Link to publication
 16:30 - 18:00 Symbolic VerificationTACAS at SUN I Chair(s): Holger Hermanns Saarland University 16:3030mTalk iRank: a variable order metric for DEDS subject to linear invariantsTACAS Link to publication 17:0030mTalk Edge-Specified Reduction Binary Decision DiagramsTACAS Link to publication 17:3030mTalk Effective Entailment Checking for Separation Logic with Inductive DefinitionsTACASJens Katelaan , Christoph Matheja RWTH Aachen University, Florian Zuleger Vienna University of Technology Link to publication

#### Thu 11 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

 10:30 - 12:30 SynthesisTACAS at SUN I Chair(s): Roland Meyer Technical University of Braunschweig 10:3030mTalk Synthesis of Symbolic Controllers: A Parallelized and Sparsity-Aware ApproachTACASMahmoud Khaled TU Munich, Eric Kim , Murat Arcak , Majid Zamani Link to publication 11:0030mTalk StocHy: automated verification and synthesis of stochastic processesTACASNathalie Cauchi University of Oxford, Alessandro Abate University of Oxford Link to publication 11:3030mTalk Minimal-Time Synthesis for Parametric Timed AutomataTACASÉtienne André LIPN, CNRS UMR 7030, Université Paris 13, Vincent Bloemen University of Twente, Laure Petrucci Université Paris 13, Jaco van de Pol Aarhus University Link to publication 12:0030mTalk Environmentally-friendly GR(1) SynthesisTACASRupak Majumdar MPI-SWS, Germany, Nir Piterman , Anne-Kathrin Schmuck Link to publication
 14:00 - 16:00 Safety and Fault-tolerant SystemsTACAS at SUN I Chair(s): Rance Cleaveland University of Maryland 14:0030mTalk Digital Bifurcation Analysis of TCP DynamicsTACASNikola Benes , Lubos Brim , Samuel Pastva , David Safranek Masaryk University Link to publication 14:3030mTalk Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model CheckingTACASIlina Stoilkovska Vienna University of Technology , Igor Konnov Inria Nancy, Josef Widder TU Wien, Florian Zuleger Vienna University of Technology Link to publication 15:0030mTalk Measuring Masking Fault-ToleranceTACASPablo Castro Dept. of Computer Science FCEFQyN, University of Rio Cuarto, Pedro D'Argenio , Ramiro Demasi , Luciano Putruele Link to publication 15:3030mTalk PhASAR: An Inter-Procedural Static Analysis Framework for C/C++TACASPhilipp Dominik Schubert Heinz Nixdorf Institut, Paderborn University, Ben Hermann University of Paderborn, Eric Bodden Heinz Nixdorf Institut, Paderborn University and Fraunhofer IEM Link to publication
 16:30 - 18:00 Monitoring and Runtime VerificationTACAS at SUN I Chair(s): Ondřej Lengál Brno University of Technology 16:3030mTalk Specification and Efficient Monitoring Beyond STLTACAS Link to publication 17:0030mTalk VyPR2: A Framework for Runtime Verification of Python Web ServicesTACASJoshua Dawes University of Manchester and CERN, Giles Reger University of Manchester, Giovanni Franzoni , Andreas Pfeiffer , Giacomo Govi Link to publication 17:3030mTalk Constraint-based Monitoring of HyperpropertiesTACASChristopher Hahn , Marvin Stenger , Leander Tentrup Saarland University Link to publication

## Call for Papers

TACAS is a forum for researchers, developers and users interested in rigorously based tools and algorithms for the construction and analysis of systems. The conference aims to bridge the gaps between different communities with this common interest and to support them in their quest to improve the utility, reliability, flexibility, and efficiency of tools and algorithms for building systems.

Theoretical papers with clear relevance for tool construction and analysis as well as tool descriptions and case studies with a conceptual message are all encouraged. The topics covered by the conference include but are not limited to:

• specification and verification techniques;
• software and hardware verification;
• analytical techniques for real-time, hybrid, or stochastic systems;
• analytical techniques for safety, security, or dependability;
• SAT and SMT solving;
• theorem-proving;
• model-checking;
• static and dynamic program analysis;
• testing;
• abstraction techniques for modelling and verification;
• compositional and refinement-based methodologies;
• system construction and transformation techniques;
• machine-learning techniques for synthesis and verification;
• tool environments and tool architectures;
• applications and case studies.

### Important dates and submission

See the Important Days of ETAPS 2019. Submit your paper via the TACAS 2019 author interface of EasyChair. Please see additional instructions on submitting through the EasyChair interface that are available once you log into EasyChair and explain how to submit an artifact, etc.

TACAS 2019 will not have a rebuttal phase.

### TACAS paper categories

TACAS accepts four types of submissions: research papers, case-study papers, regular tool papers, and tool-demonstration papers. Papers of all four types will appear in the proceedings and have presentations during the conference.

• Research papers clearly identify and justify a principled advance to the theoretical foundations for the construction and analysis of systems. Where applicable, they are supported by experimental validation.

• Case-study papers report on case studies, preferably in a real-world setting. They should provide information about the following aspects: the system being studied and the reasons why it is of interest, the goals of the study, the challenges the system poses to automated analysis/testing/synthesis, research methodologies and approaches used, the degree to which the goals were met, and how the results can be generalized to other problems and domains.

• Regular tool papers present a new tool, a new tool component, or novel extensions to an existing tool, and are subject to an artifact submission requirement (see below). They should provide a short description of the theoretical foundations with relevant citations, and emphasize the design and implementation concerns, including software architecture and core data structures. A regular tool paper should give a clear account of the tool’s functionality, discuss the tool’s practical capabilities with reference to the type and size of problems it can handle, describe experience with realistic case studies, and where applicable, provide a rigorous experimental evaluation. Papers that present extensions to existing tools should clearly focus on the improvements or extensions with respect to previously published versions of the tool, preferably substantiated by data on enhancements in terms of resources and capabilities.

• Tool demonstration papers focus on the usage aspects of tools and are also subject to an artifact submission requirement (see below). Theoretical foundations and experimental evaluation are not required, however, a motivation as to why the tool is interesting and significant should be provided. Further, the paper should describe aspects such as, for example, the assumptions about application domain and/or extent of potential generality, demonstrate the tool workflow(s), explain integration and/or human interaction, evaluate the overall role and the impact to the development process.

### Paper length limits

The length of research, case-study, and regular tool papers is limited to 15 pages in the LNCS format, excluding the blibliography. The length of tool-demonstration papers is limited to 6 pages in the LNCS format, including the bibliography.

Appendices going beyond the above page limits are not allowed! Additional (unlimited) appendices can be made available separately or as part of an extended version of the paper made available via arXiv, Zenodo, or a similar service, and cited in the paper. The reviewers are, however, not obliged to read such appendices.

### Tool paper artifact submission

This year, authors of regular tool papers and tool-demonstration papers are required to provide an artifact (format described below) with their submission. In this case, the artifact has to be submitted together with the submission to be reviewed (i.e., by Nov. 16, 2018). The artifact will be evaluated by the artifact evaluation committee (AEC) independently of the paper. The results of the artifact evaluation will be taken into account during discussion of the paper submission.

Exceptions to this rule may be granted by the PC chairs, but only in cases when the tool cannot be in any reasonable way run by the AEC. In such cases, the authors should contact the PC chairs as soon as possible (at least 7 days prior to abstract submission), ask for an exception, and explain why it is needed. An example of a case where an exception can be negotiated is a tool that must be run in some very special environment, e.g., on special hardware that cannot be virtualised in any way. Note that license problems are generally not an acceptable grounds for an exception. When an exception is granted, the authors should instead submit a detailed video showing their tool in action.

The submission page for tool paper artifacts will be opened after the abstract submission deadline.

### Posters and tool demonstrations

Subject to available space, authors of all accepted papers will be given an option to present their results in the form of a poster in addition to the talk. Moreover, again subject to available space, authors of regular tool papers and tool demonstration papers will be given an option to demonstrate their tool to conference participants in addition to giving their talk / presenting their poster. More information about the posters and demonstrations will be posted to the concerned authors in due time.

### Submission and evaluation criteria

Evaluation: All papers will be evaluated by the program committee, coordinated by the PC chairs, aided by the case-study chair for case-study papers, and by the tools chair for regular tool papers and tool demonstration papers. All papers will be judged on novelty, significance, correctness, and clarity.

Replicability of results: Reproducibility of results is of the utmost importance for the TACAS community. Therefore, we encourage all authors of submitted papers to include support for replicating the results of their papers. For theorems, this would mean providing proofs; for algorithms, this would mean including evidence of correctness and acceptable performance, either by a theoretical analysis or by experimentation; and for experiments, one should provide access to the artifacts used to generate the experimental data. Material that does not fit into the paper may be provided on a supplementary web site, with access appropriately enabled and license rights made clear. For example, the supplemental material for reviewing case-study papers and papers with experimental results could be classified as reviewer-confidential if necessary (e.g., if proprietary data are investigated or software is not open source). In general, TACAS encourages all authors to archive additional material and make it citable via DOI (e.g., via Zenodo or Figshare).

Limit of 3 submissions: Each individual author is limited to a maximum of three submissions as an author or co-author. Authors of co-authored submissions are jointly responsible for respecting this policy. In case of violations, all submissions of this (co-)author will be desk-rejected.

### Artifact evaluation

Artifact evaluation is compulsory for regular tool papers and tool-demonstration papers. Authors of all accepted research papers and case-study papers will be invited to submit (but are not required to) the relevant artifact for evaluation by the AEC. The AEC will read the paper and evaluate the artifact according to the following criteria:

• consistency with and replicability of results in the paper,
• completeness,
• documentation, and
• ease of use.

### Competition on software verification

TACAS 2019 hosts the 8th Competition on Software Verification with the goal to evaluate technology transfer and compare state-of-the-art software verifiers with respect to effectiveness and efficiency. More information can be found on the webpage of the competition.

As in 2018, TACAS’19 will include artifact evaluation for all types of papers. For regular tool papers and tool demonstration papers, artifact evaluation is compulsory (see the TACAS’19 call for papers), for research and case-study papers, it is voluntary (papers with accepted artifacts will receive a badge).

# Important Dates

• Tool papers:
• 9 November 2018: deadline for abstract submission
• 16 November 2018: deadline for paper submission
• 30 November 2018: request for clarification (if AEC members encounter technical problems evaluating the artifact, authors will be asked to submit clarifying instructions)
• 7 December 2018: clarification submission deadline
• 25 January 2019: TACAS author notification
• Research and case study papers:
• 30 January 2019: deadline for artifact submission
• 14 February 2019: Notification of authors

## Compulsary Artifact Evaluation for Regular Tool Papers and Tool Demonstration Papers

In TACAS’19, regular tool papers and tool-demonstration papers are required to be accompanied by an artifact for evaluation by the Artifact Evaluation Committee (AEC). An artifact is any additional material (software, data sets, machine-checkable proofs, etc.) that substantiates the claims made in the paper and ideally makes them fully replicable. As an example, a typical artifact would consist of the tool (in binary or source code form) and its documentation, the input files (e.g., models analysed or programs verified) used for the tool evaluation in the paper, and a configuration file or document describing the parameters used in the experiments. The AEC will read the submitted paper and evaluate the submitted artifact w.r.t. the following criteria:

• consistency with and replicability of results presented in the paper,
• completeness,
• documentation, and
• ease of use.

Results of the evaluation will be taken into consideration during the review phase of TACAS’19. Papers that succeed in artifact evaluation and are accepted will receive a badge. The fact that not all experiments are reproducible (e.g., due to high computational demands) does not mean automatic rejection of the paper.

## Artifact Evaluation for Research and Case-Study Papers

Authors of all accepted research papers and case-study papers for TACAS’19 will also be invited to submit an artifact (in this case, the submission is voluntary). The artifact will be evaluated using the same criteria as above. Authors of artifacts that are accepted by the AEC will receive a badge that can be shown on the title page of the corresponding paper. Due to the very short time for reviewing the artifacts, there will be no rebuttal (difference from TACAS’18). Therefore, please make the review process as easy for the reviewers as possible, preferably using easy-to-use scripts that, e.g., run the experiments that you report on in the paper and draw tables/graphs from the results that are similar to the tables and graphs in your paper (the reviewers will not study your paper and artifact in detail to know how to interpret the output data).

## Artifact Submission

An artifact submission consists of

• an abstract that summarizes the artifact and its relation to the paper,
• [for research and case-study papers] a .pdf file of the accepted paper (uploaded via EasyChair), which may be modified from the submitted version to take reviewers’ comments into account (for tool papers, the submitted .pdf file will be used),
• a directory with the artifact itself,
• a text file LICENSE that contains the license for the artifact (it is required that the license at least allows the AEC to evaluate the artifact w.r.t. the criteria mentioned above),
• a text file README that contains detailed, step-by-step instructions on how to use the artifact to replicate the results in the paper, and
• SHA-256 hash of the zip file.

Tool paper artifacts are submitted using the TACAS 2019 author interface of EasyChair (into the TACAS 2019 AE for non-tool papers track). When submitting, please fill in the same information as for the submitted paper.

## Guidelines for Artifacts

We expect artifact submissions to package their artifact and write their instructions such that AEC members can evaluate the artifact using the TACAS 2019 Artifact Evaluation Virtual Machine for VirtualBox available here (login/password: “tacas19” / “a”, same password for root access). The virtual machine is based on Ubuntu 18.04.1 LTS GNU/Linux operating system with the following additional packages: build-essential, cmake, clang, mono-complete, openjdk-8-jdk, ruby, and a 32-bit libc. Moreover, VirtualBox guest additions are installed on the VM, it is therefore possible to connect a shared folder from the host computer (see a how-to file in the HOME directory).

If the artifact requires additional software or libraries that are not part of the virtual machine, these need to be included in the .zip file (e.g. in the form of Debian packages) and the instructions must include all necessary steps for their installation and setup (see the FAQ below for hints). AEC members will not download software or data from external sources, and the artifact must work without a network connection. In case you feel that this VM will not allow an adequate replication of the results in your paper, please contact the AEC co-chairs prior to artifact submission.

It is to the advantage of authors to prepare an artifact that is easy to evaluate by the AEC. Some guidelines:

• Document in detail how to replicate most, or ideally all, of the (experimental) results of the paper using the artifact.
• Keep the evaluation process simple through easy-to-use scripts and provide detailed documentation assuming minimum expertise of users.
• For experiments that require a large amount of resources (hardware or time), it is recommended to provide a way to replicate a subset of the results of the paper with reasonably modest resources (RAM, number of cores), so that the results can be reproduced on various hardware platforms including laptops, and in a reasonable amount of time.
• State the resource requirements, or the environment in which you successfully tested the artifact, in the instructions file (RAM, number of cores, CPU frequency).

Members of the AEC will use the submitted artifact for the sole purpose of artifact evaluation, We do, however, encourage authors to make their artifacts publicly and permanently available.

## FAQ

Q: So, I am supposed to install our tool in the provided VM and then provide a link to the modified VM, right?

A: No, you are supposed to create a .zip file with the tool and all dependencies. The reviewers will download the vanilla TACAS’19 VM, copy your .zip file there, and setup your tool according to the README file.

Q: How can I install packages without an Internet connection?

A: For Debian packages (.deb files), you can just add them to the .zip file and install them using

$sudo dpkg -i <file>  For instance, to download Octave with all dependencies, you can proceed, e.g., as follows: $ mkdir packages
$cd packages$ sudo apt-get update
$apt-get --print-uris install octave | grep "^'" | sed "s/^'$$[^']*$$'.*$/\1/g" > octave.deps
$for i in$(cat octave.deps) ; do wget -nv $i ; done  The downloaded packages can then be installed using $ cd packages
$sudo dpkg -i *.deb  For Python, you can, e.g., use pip to download the packages. For instance, to download the bitarray package, you can run (we assume you have pip installed) $ pip download bitarray


\$ pip install bitarray-0.8.3.tar.gz