Linear-Time Verification of Data-Aware Dynamic Systems with Arithmetic
Authors: Paolo Felli, Marco Montali, Sarah Winkler5642-5650
AAAI 2022 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Finally, we demonstrate the feasibility of our approach in a prototype implementation. and We implemented our approach in the prototype ada (arithmetic DDS analyzer), available via a web interface (https://ltl.adatool.dev) where source code and examples can be found. ... In the extended version (Felli, Montali, and Winkler 2021) we show results for relevant examples, including Ex. 1.1 and processes converted from Petri nets with data (Mannhardt et al. 2016). |
| Researcher Affiliation | Academia | Paolo Felli, Marco Montali, Sarah Winkler* Free University of Bozen-Bolzano Bolzano Italy {pfelli,montali,winkler}@inf.unibz.it |
| Pseudocode | No | The paper does not contain structured pseudocode or algorithm blocks. |
| Open Source Code | Yes | We implemented our approach in the prototype ada (arithmetic DDS analyzer), available via a web interface (https://ltl.adatool.dev) where source code and examples can be found. |
| Open Datasets | No | The paper mentions 'relevant examples, including Ex. 1.1 and processes converted from Petri nets with data (Mannhardt et al. 2016)' but does not provide concrete access information (links, DOIs, specific citations for datasets) for publicly available datasets used for training or evaluation. |
| Dataset Splits | No | The paper does not provide specific dataset split information (exact percentages, sample counts, citations to predefined splits, or detailed splitting methodology). |
| Hardware Specification | No | The paper does not provide specific hardware details (exact GPU/CPU models, processor types, or memory amounts) used for running its experiments. |
| Software Dependencies | No | The paper states 'ada is written in Python and uses the Z3 SMT solver (de Moura and Bjørner 2008),' but it does not provide explicit version numbers for Python or Z3, which are required for a reproducible description. |
| Experiment Setup | No | The paper describes the theoretical framework and implementation of a prototype tool ('ada') but does not provide specific experimental setup details such as concrete hyperparameter values, training configurations, or system-level settings for its examples or evaluations. |