List of Artifacts for TACAS Articles
Download table in CSV format.
The list below is restricted to those artifacts that are identifiable with a DOI. The above table contains all artifacts.
| Year | Article | Artifact | Title (Article or Artifact) | Badge | |
| 2021 |  |
 10.1007/978-3-0… |
10.6084/m9.figs… |
Directed Reachability for Infinite-State Systems |  |
| 2021 | |
10.1007/978-3-0… |
10.5281/zenodo.… |
SyReNN: A Tool for Analyzing Deep Neural Networks | |
| 2021 | |
10.1007/978-3-0… |
10.5281/zenodo.… |
MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers | |
| 2021 | |
10.1007/978-3-0… |
10.5281/zenodo.… |
dtControl 2.0: Explainable Strategy Representation via Decision Tree L… | |
| 2021 | |
10.1007/978-3-0… |
10.6084/m9.figs… |
Replicating RESTART with Prolonged Retrials: An Experimental Report | |
| 2021 | |
10.1007/978-3-0… |
10.6084/m9.figs… |
A Web Interface for Petri Nets with Transits and Petri Games | |
| 2021 | |
10.1007/978-3-0… |
10.5281/zenodo.… |
Momba: JANI Meets Python | |
| 2021 | |
10.1007/978-3-0… |
10.5281/zenodo.… |
Software Verification: 10th Comparative Evaluation (SV-COMP 2021) (SV-… |  |
| 2021 | |
10.1007/978-3-0… |
10.5281/zenodo.… |
Software Verification: 10th Comparative Evaluation (SV-COMP 2021) (Res… | |
| 2021 | |
10.1007/978-3-0… |
10.5281/zenodo.… |
Software Verification: 10th Comparative Evaluation (SV-COMP 2021) (Ver… | |
| 2021 | |
10.1007/978-3-0… |
10.5281/zenodo.… |
Software Verification: 10th Comparative Evaluation (SV-COMP 2021) (Ben… | |
| 2021 | |
10.1007/978-3-0… |
10.5281/zenodo.… |
cpalockator: Thread-Modular Analysis with Projections - (Competition C… | |
| 2021 | |
10.1007/978-3-0… |
10.5281/zenodo.… |
Dartagnan: Leveraging Compiler Optimizations and the Price of Precisio… | |
| 2021 | |
10.1007/978-3-0… |
10.5281/zenodo.… |
Gazer-Theta: LLVM-based Verifier Portfolio with BMC/CEGAR (Competition… | |
| 2021 | |
10.1007/978-3-0… |
10.5281/zenodo.… |
Towards String Support in JayHorn (Competition Contribution) | |
| 2021 | |
10.1007/978-3-0… |
10.5281/zenodo.… |
JDart: Portfolio Solving, Breadth-First Search and SMT-Lib Strings (Co… | |
| 2021 | |
10.1007/978-3-0… |
10.5281/zenodo.… |
Symbiotic 8: Beyond Symbolic Execution - (Competition Contribution) | |
| 2021 | |
10.1007/978-3-0… |
10.5281/zenodo.… |
TACAS 2021 Artifact Evaluation VM | n/a |
| 2021 | |
10.1007/978-3-0… |
10.5281/zenodo.… |
Inductive Synthesis for Probabilistic Programs Reaches New Horizons | |
| 2021 | |
10.1007/978-3-0… |
10.5281/zenodo.… |
Multi-objective Optimization of Long-run Average and Total Rewards | |
| 2021 | |
10.1007/978-3-0… |
10.5281/zenodo.… |
Iterative Bounded Synthesis for Efficient Cycle Detection in Parametri… | |
| 2021 | |
10.1007/978-3-0… |
10.5281/zenodo.… |
Resilient Capacity-Aware Routing | |
| 2020 | |
10.1007/978-3-0… |
10.5281/zenodo.… |
Software Verification with PDR: An Implementation of the State of the … |  |
| 2020 | |
10.1007/978-3-0… |
10.6084/m9.figs… |
Verifying Array Manipulating Programs with Full-Program Induction | |
| 2020 | |
10.1007/978-3-0… |
10.5281/zenodo.… |
Interpretation-Based Violation Witness Validation for C: NITWIT | |
| 2020 | |
10.1007/978-3-0… |
10.5281/zenodo.… |
A Calculus for Modular Loop Acceleration – Artifact Evaluation | |
| 2020 | |
10.1007/978-3-0… |
10.6084/m9.figs… |
Multi-Agent Safety Verification using Symmetry Transformations | |
| 2020 | |
10.1007/978-3-0… |
10.5281/zenodo.… |
Structural Invariants for the Verification of Systems with Parameteriz… | |
| 2020 | |
10.1007/978-3-0… |
10.4121/uuid:36… |
Automated Verification of Parallel Nested DFS | |
| 2020 | |
10.1007/978-3-0… |
10.6084/m9.figs… |
Good-for-MDPs Automata for Probabilistic Analysis and Reinforcement Le… | |
| 2020 | |
10.1007/978-3-0… |
10.6084/m9.figs… |
Simple Strategies in Multi-Objective MDPs | |
| 2020 | |
10.1007/978-3-0… |
10.6084/m9.figs… |
Artifact for Partial Order Reduction for Deep Bug Finding in Synchrono… | |
| 2020 | |
10.1007/978-3-0… |
10.6084/m9.figs… |
KReach: A Tool for Reachability in Petri Nets | |
| 2020 | |
10.1007/978-3-0… |
10.5281/zenodo.… |
AVR: Abstractly Verifying Reachability | |
| 2020 | |
10.1007/978-3-0… |
10.5281/zenodo.… |
Artifact for "Towards Practical Verification of Reachability Checking … | |
| 2020 | |
10.1007/978-3-0… |
10.6084/m9.figs… |
Learning One-Clock Timed Automata | |
| 2020 | |
10.1007/978-3-0… |
10.6084/m9.figs… |
An O(m log n) algorithm for branching bisimilarity on labelled transit… | |
| 2020 | |
10.1007/978-3-0… |
10.6084/m9.figs… |
Artifact Evaluation for Verifying Quantum Communication Protocols with… | |
| 2020 | |
10.1007/978-3-0… |
10.5281/zenodo.… |
Highly Automated Formal Proofs over Memory Usage of Assembly Code | |
| 2020 | |
10.1007/978-3-0… |
10.0.23.196/m9.… |
GASOL: Gas Analysis and Optimization for Ethereum Smart Contracts (Art… | |
| 2020 | |
10.1007/978-3-0… |
10.5281/zenodo.… |
CPU Energy Meter: A Tool for Energy-Aware Algorithms Engineering (2nd … | |
| 2020 | |
10.1007/978-3-0… |
10.5281/zenodo.… |
Verifying OpenJDK's LinkedList using KeY | |
| 2020 | |
10.1007/978-3-0… |
10.5281/zenodo.… |
Analysing installation scenarios of Debian packages | |
| 2020 | |
10.1007/978-3-0… |
10.6084/m9.figs… |
Describing and Simulating Concurrent Quantum Systems (artifact resubmi… | |
| 2020 | |
10.1007/978-3-0… |
10.5281/zenodo.… |
EMTST: Engineering the Meta-theory of Session Types | |
| 2020 | |
10.1007/978-3-0… |
10.5281/zenodo.… |
Advances in Automatic Software Verification: SV-COMP 2020 (SV-Benchmar… |  |
| 2020 | |
10.1007/978-3-0… |
10.5281/zenodo.… |
Advances in Automatic Software Verification: SV-COMP 2020 (Results) | |
| 2020 | |
10.1007/978-3-0… |
10.5281/zenodo.… |
Advances in Automatic Software Verification: SV-COMP 2020 (Verificatio… | |
| 2020 | |
10.1007/978-3-0… |
10.5281/zenodo.… |
2LS: Heap Analysis and Memory Safety - (Competition Contribution) | |
| 2020 | |
10.1007/978-3-0… |
10.5281/zenodo.… |
COASTAL: Combining Concolic and Fuzzing for Java (Competition Contribu… | |
| 2020 | |
10.1007/978-3-0… |
10.5281/zenodo.… |
Dartagnan: Bounded Model Checking for Weak Memory Models (Competition … | |
| 2020 | |
10.1007/978-3-0… |
10.5281/zenodo.… |
GACAL: Conjecture-Based Verification - (Competition Contribution) | |
| 2020 | |
10.1007/978-3-0… |
10.5281/zenodo.… |
Java Ranger at SV-COMP 2020 (Competition Contribution) | |
| 2020 | |
10.1007/978-3-0… |
10.5281/zenodo.… |
JDart: Dynamic Symbolic Execution for Java Bytecode (Competition Contr… | |
| 2020 | |
10.1007/978-3-0… |
10.5281/zenodo.… |
Map2Check: Using Symbolic Execution and Fuzzing - (Competition Contrib… | |
| 2020 | |
10.1007/978-3-0… |
10.5281/zenodo.… |
PredatorHP Revamped (Not Only) for Interval-Sized Memory Regions and M… | |
| 2020 | |
10.1007/978-3-0… |
10.5281/zenodo.… |
Symbiotic 7: Integration of Predator and More - (Competition Contribut… | |
| 2020 | |
10.1007/978-3-0… |
10.5281/zenodo.… |
Ultimate Taipan with Symbolic Interpretation and Fluid Abstractions - … | |
| 2019 | |
10.1007/978-3-0… |
10.6084/m9.figs… |
TACAS 2019 Artifact Evaluation VM | n/a |
| 2019 | |
10.1007/978-3-0… |
10.6084/m9.figs… |
Multi-core On-the-fly Saturation | |
| 2019 | |
10.1007/978-3-0… |
10.6084/m9.figs… |
Computing the Expected Execution Time of Probabilistic Workflow Nets | |
| 2019 | |
10.1007/978-3-0… |
10.6084/m9.figs… |
Isabelle/HOL proof and Apache Flink program for TACAS 2019 paper: Comp… | |
| 2019 | |
10.1007/978-3-0… |
10.6084/m9.figs… |
ILAng: A Modeling and Verification Platform for SoCs using Instruction… | |
| 2019 | |
10.1007/978-3-0… |
10.6084/m9.figs… |
Minimal-Time Synthesis for Parametric Timed Automata | |
| 2019 | |
10.1007/978-3-0… |
10.6084/m9.figs… |
StocHy: automated verification and synthesis of stochastic processes | |
| 2019 | |
10.1007/978-3-0… |
10.6084/m9.figs… |
Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded M… | |
| 2019 | |
10.1007/978-3-0… |
10.6084/m9.figs… |
PhASAR: An Inter-Procedural Static Analysis Framework for C/C++ | |
| 2019 | |
10.1007/978-3-0… |
10.5281/zenodo.… |
Automatic Verification of C and Java Programs: SV-COMP 2019 (Verificat… | n/a |
| 2018 | |
10.1007/978-3-3… |
10.6084/m9.figs… |
Verified Model Checking of Timed Automata | |
| 2018 | |
10.1007/978-3-3… |
10.6084/m9.figs… |
CDCLSym: Introducing Effective Symmetry Breaking in SAT Solving | |
| 2018 | |
10.1007/978-3-3… |
10.6084/m9.figs… |
Bit-Vector Model Counting using Statistical Estimation | none |
| 2018 | |
10.1007/978-3-3… |
10.6084/m9.figs… |
A Verified Implementation of the Bounded List Container | none |
| 2018 | |
10.1007/978-3-3… |
10.6084/m9.figs… |
Automating Deductive Verification for Weak-Memory Programs (artifact) | |
| 2018 | |
10.1007/978-3-3… |
10.6084/m9.figs… |
Invariant Synthesis for Incomplete Verification Engines | |
| 2018 | |
10.1007/978-3-3… |
10.6084/m9.figs… |
More Scalable LTL Model Checking via Discovering Design-Space Dependen… | |
| 2018 | |
10.1007/978-3-3… |
10.6084/m9.figs… |
Generation of Minimum Tree-like Witnesses for Existential CTL | |
| 2018 | |
10.1007/978-3-3… |
10.6084/m9.figs… |
PESTS: Partial Evaluator of Simple Transition Systems | |
| 2018 | |
10.1007/978-3-3… |
10.6084/m9.figs… |
ICE-based Refinement Type Discovery for Higher-Order Functional Progra… | |
| 2018 | |
10.1007/978-3-3… |
10.6084/m9.figs… |
Strategy Representation by Decision Trees in Reactive Synthesis | none |
| 2018 | |
10.1007/978-3-3… |
10.6084/m9.figs… |
EMME: a formal tool for ECMAScript Memory Model Evaluation | |
| 2018 | |
10.1007/978-3-3… |
10.6084/m9.figs… |
Abstraction Refinement for Emptiness Checking of Alternating Data Auto… | none |
| 2018 | |
10.1007/978-3-3… |
10.6084/m9.figs… |
Revisiting Enumerative Instantiation | |
| 2018 | |
10.1007/978-3-3… |
10.6084/m9.figs… |
A Non-linear Arithmetic Procedure for Control-Command Software Verific… | |
| 2018 | |
10.1007/978-3-3… |
10.6084/m9.figs… |
Approximate Reduction of Finite Automata for High-Speed Network Intrus… | |
| 2018 | |
10.1007/978-3-3… |
10.6084/m9.figs… |
Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Co… | |
| 2018 | |
10.1007/978-3-3… |
10.6084/m9.figs… |
Artifact For The Refinement Calculus of Reactive Systems Toolset | |
| 2018 | |
10.1007/978-3-3… |
10.6084/m9.figs… |
Optimal Dynamic Partial Order Reduction with Observers | |
| 2018 | |
10.1007/978-3-3… |
10.6084/m9.figs… |
Multi-Cost Bounded Reachability in MDPs | |
| 2018 | |
10.1007/978-3-3… |
10.4121/uuid:64… |
A Statistical Model Checker for Nondeterminism and Rare Events (Artifa… | |
| 2018 | |
10.1007/978-3-3… |
10.6084/m9.figs… |
Permutation Games for the Weakly Aconjunctive mu-Calculus | |