| 1. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Adding time to pushdown automata
- 2012
-
Ingår i: Quantities in Formal Methods. ; , s. 1-16
-
Konferensbidrag (refereegranskat)
|
|
| 2. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Budget-bounded model-checking pushdown systems
- 2014
-
Ingår i: Formal methods in system design. - : Springer Science and Business Media LLC. - 0925-9856 .- 1572-8102. ; 45:2, s. 273-301
-
Tidskriftsartikel (refereegranskat)abstract
- We address the verification problem for concurrent programs modeled as multi-pushdown systems (MPDS). In general, MPDS are Turing powerful and hence come along with undecidability of all basic decision problems. Because of this, several subclasses of MPDS have been proposed and studied in the literature (Atig et al. in LNCS, Springer, Berlin, 2005; La Torre et al. in LICS, IEEE, 2007; Lange and Lei in Inf Didact 8, 2009; Qadeer and Rehof in TACAS, LNCS, Springer, Berlin, 2005). In this paper, we propose the class of bounded-budget MPDS, which are restricted in the sense that each stack can perform an unbounded number of context switches only if its depth is below a given bound, and a bounded number of context switches otherwise. We show that the reachability problem for this subclass is Pspace-complete and that LTL-model-checking is Exptime-complete. Furthermore, we propose a code-to-code translation that inputs a concurrent program and produces a sequential program such that running under the budget-bounded restriction yields the same set of reachable states as running . Moreover, detecting (fair) non-terminating executions in can be reduced to LTL-Model-Checking of . By leveraging standard sequential analysis tools, we have implemented a prototype tool and applied it on a set of benchmarks, showing the feasibility of our translation.
|
|
| 3. |
|
|
| 4. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Dense-Timed Pushdown Automata
- 2012
-
Ingår i: Proc. 27th ACM/IEEE Symposium on Logic in Computer Science. - : IEEE Computer Society. - 9780769547695 ; , s. 35-44
-
Konferensbidrag (refereegranskat)abstract
- We propose a model that captures the behavior of real-time recursive systems. To that end, we introduce dense-timed pushdown automata that extend the classical models of pushdown automata and timed automata, in the sense that the automaton operates on a finite set of real-valued clocks, and each symbol in the stack is equipped with a real-valued clock representing its "age". The model induces a transition system that is infinite in two dimensions, namely it gives rise to a stack with an unbounded number of symbols each of which with a real-valued clock. The main contribution of the paper is an EXPTIME-complete algorithm for solving the reachability problem for dense-timed pushdown automata.
|
|
| 5. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Multi-Pushdown Systems with Budgets
- 2012
-
Ingår i: Formal Methods in Computer-Aided Design. ; , s. 24-33
-
Konferensbidrag (refereegranskat)
|
|
| 6. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Norn: An SMT Solver for String Constraints
- 2015
-
Ingår i: COMPUTER AIDED VERIFICATION, PT I. - Cham : SPRINGER-VERLAG BERLIN. - 9783319216904 - 9783319216898 ; , s. 462-469
-
Konferensbidrag (refereegranskat)abstract
- We present version 1.0 of the Norn SMT solver for string constraints. Norn is a solver for an expressive constraint language, including word equations, length constraints, and regular membership queries. As a feature distinguishing Norn from other SMT solvers, Norn is a decision procedure under the assumption of a set of acyclicity conditions on word equations, without any restrictions on the use of regular membership.
|
|
| 7. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
String Constraints for Verification
- 2014
-
Ingår i: <em>26th International Conference on Computer Aided Verification (CAV 2014), Vienna, Austria, Jul. 9-12, 2014.</em>. - Berlin : Springer. - 9783319088662 - 9783319088679 ; , s. 150-166
-
Konferensbidrag (refereegranskat)abstract
- We present a decision procedure for a logic that combines (i) word equations over string variables denoting words of arbitrary lengths, together with (ii) constraints on the length of words, and on (iii) the regular languages to which words belong. Decidability of this general logic is still open. Our procedure is sound for the general logic, and a decision procedure for a particularly rich fragment that restricts the form in which word equations are written. In contrast to many existing procedures, our method does not make assumptions about the maximum length of words. We have developed a prototypical implementation of our decision procedure, and integrated it into a CEGAR-based model checker for the analysis of programs encoded as Horn clauses. Our tool is able to automatically establish the correctness of several programs that are beyond the reach of existing methods.
|
|
| 8. |
|
|
| 9. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Zenoness for Timed Pushdown Automata
- 2014
-
Ingår i: Proceedings 15th International Workshop on Verification of Infinite-State Systems, {INFINITY} 2013, Hanoi, Vietnam, 14th October 2013.. ; , s. -47
-
Konferensbidrag (refereegranskat)abstract
- Timed pushdown automata are pushdown automata extended with a finite set of real-valued clocks. Additionaly, each symbol in the stack is equipped with a value representing its age. The enabledness of a transition may depend on the values of the clocks and the age of the topmost symbol. Therefore, dense-timed pushdown automata subsume both pushdown automata and timed automata. We have previously shown that the reachability problem for this model is decidable. In this paper, we study the zenoness problem and show that it is EXPTIME-complete.
|
|
