مؤتمر
Revisiting Underapproximate Reachability for Multipushdown Systems
| العنوان: | Revisiting Underapproximate Reachability for Multipushdown Systems |
|---|---|
| المؤلفون: | Akshay, S., Gastin, Paul, Krishna, S, Roychowdhury, Sparsa |
| المساهمون: | Indian Institute of Technology Bombay (IIT Bombay), Laboratoire Spécification et Vérification (LSV), Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Research Lab in Computer Science (ReLaX), Institute of Mathematical Sciences Chennai (IMSc)-Chennai Mathematical Institute Inde -Université de Bordeaux (UB)-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Partly supported by IRL ReLaX |
| المصدر: | 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'20) Tools and Algorithms for the Construction and Analysis of Systems (TACAS) https://hal.science/hal-04540223Test Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Apr 2020, Dublin, Ireland. pp.387-404, ⟨10.1007/978-3-030-45190-5_21⟩ |
| بيانات النشر: | HAL CCSD Springer International Publishing |
| سنة النشر: | 2020 |
| مصطلحات موضوعية: | Multipushdown Systems, Underapproximate Reachability, Timed pushdown automata, [INFO]Computer Science [cs] |
| جغرافية الموضوع: | Dublin, Ireland |
| الوصف: | International audience ; Boolean programs with multiple recursive threads can be captured aspushdown automata with multiple stacks. This model is Turing complete, andhence, one is often interested in analyzing a restricted class that stillcaptures useful behaviors. In this paper, we propose a new class of boundedunderapproximations for multi-pushdown systems, which subsumes most existingclasses. We develop an efficient algorithm for solving the under-approximatereachability problem, which is based on efficient fix-point computations. Weimplement it in our tool \trim{} and illustrate its applicability bygenerating a set of relevant benchmarks and examining its performance. As anadditional takeaway \trim{} solves the binary reachability problem in pushdownautomata. To show the versatility of our approach, we then extend ouralgorithm to the timed setting and provide the first implementation that canhandle timed multi-pushdown automata with closed guards. |
| نوع الوثيقة: | conference object |
| اللغة: | English |
| العلاقة: | info:eu-repo/semantics/altIdentifier/arxiv/2002.05950; hal-04540223; https://hal.science/hal-04540223Test; ARXIV: 2002.05950 |
| DOI: | 10.1007/978-3-030-45190-5_21 |
| الإتاحة: | https://doi.org/10.1007/978-3-030-45190-5_21Test https://hal.science/hal-04540223Test |
| حقوق: | http://creativecommons.org/licenses/by-nc-ndTest/ |
| رقم الانضمام: | edsbas.B6394486 |
| قاعدة البيانات: | BASE |
| DOI: | 10.1007/978-3-030-45190-5_21 |
|---|