uu.seUppsala University Publications
Change search
Link to record
Permanent link

Direct link
BETA
Stenman, Jari
Publications (8 of 8) Show all publications
Abdulla, P. A., Atig, M. F., Chen, Y.-F., Holík, L., Rezine, A., Rümmer, P. & Stenman, J. (2015). Norn: An SMT solver for string constraints. In: Computer Aided Verification: Part I. Paper presented at CAV 2015, July 18–24, San Francisco, CA (pp. 462-469). Springer
Open this publication in new window or tab >>Norn: An SMT solver for string constraints
Show others...
2015 (English)In: Computer Aided Verification: Part I, Springer, 2015, p. 462-469Conference paper, Published paper (Refereed)
Abstract [en]

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.

Place, publisher, year, edition, pages
Springer, 2015
Series
Lecture Notes in Computer Science ; 9206
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-272325 (URN)10.1007/978-3-319-21690-4_29 (DOI)000364182900029 ()978-3-319-21689-8 (ISBN)
Conference
CAV 2015, July 18–24, San Francisco, CA
Projects
UPMARC
Available from: 2015-07-16 Created: 2016-01-13 Last updated: 2018-01-10Bibliographically approved
Abdulla, P. A., Atig, M. F., Rezine, O. & Stenman, J. (2014). Budget-bounded model-checking pushdown systems. Formal methods in system design, 45(2), 273-301
Open this publication in new window or tab >>Budget-bounded model-checking pushdown systems
2014 (English)In: Formal methods in system design, ISSN 0925-9856, E-ISSN 1572-8102, Vol. 45, no 2, p. 273-301Article in journal (Refereed) Published
Abstract [en]

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.

National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-234422 (URN)10.1007/s10703-014-0207-y (DOI)000343210700007 ()
Projects
UPMARCConcurrent recursive programs
Funder
Swedish Research Council
Available from: 2014-04-25 Created: 2014-10-17 Last updated: 2018-01-11
Abdulla, P. A., Atig, M. F. & Stenman, J. (2014). Computing optimal reachability costs in priced dense-timed pushdown automata. In: Language and Automata Theory and Applications: LATA 2014. Paper presented at LATA 2014, March 10–14, Madrid, Spain (pp. 62-75). Springer Berlin/Heidelberg
Open this publication in new window or tab >>Computing optimal reachability costs in priced dense-timed pushdown automata
2014 (English)In: Language and Automata Theory and Applications: LATA 2014, Springer Berlin/Heidelberg, 2014, p. 62-75Conference paper, Published paper (Refereed)
Place, publisher, year, edition, pages
Springer Berlin/Heidelberg, 2014
Series
Lecture Notes in Computer Science ; 8370
National Category
Computer Systems
Identifiers
urn:nbn:se:uu:diva-238135 (URN)10.1007/978-3-319-04921-2_5 (DOI)000352688800005 ()978-3-319-04920-5 (ISBN)
Conference
LATA 2014, March 10–14, Madrid, Spain
Projects
UPMARC
Available from: 2014-12-09 Created: 2014-12-09 Last updated: 2015-05-13Bibliographically approved
Abdulla, P. A., Atig, M. F. & Stenman, J. (2014). Zenoness for Timed Pushdown Automata. In: Proceedings 15th International Workshop on Verification of Infinite-State Systems, {INFINITY} 2013, Hanoi, Vietnam, 14th October 2013.: . Paper presented at Infinity 2014.
Open this publication in new window or tab >>Zenoness for Timed Pushdown Automata
2014 (English)In: Proceedings 15th International Workshop on Verification of Infinite-State Systems, {INFINITY} 2013, Hanoi, Vietnam, 14th October 2013., 2014, p. -47Conference paper, Published paper (Refereed)
Abstract [en]

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.

Keywords
Timed Systems, Pushdown automata
National Category
Computer Systems
Research subject
Computer Science
Identifiers
urn:nbn:se:uu:diva-238136 (URN)10.4204/EPTCS.140 (DOI)
Conference
Infinity 2014
Projects
UPMARC
Available from: 2014-12-09 Created: 2014-12-09 Last updated: 2014-12-17
Abdulla, P. A., Atig, M. F. & Stenman, J. (2012). Adding time to pushdown automata. In: Quantities in Formal Methods: QFM 2012. Paper presented at Workshop on Quantities in Formal Methods 2012 (pp. 1-16).
Open this publication in new window or tab >>Adding time to pushdown automata
2012 (English)In: Quantities in Formal Methods: QFM 2012, 2012, p. 1-16Conference paper, Published paper (Refereed)
Series
Electronic Proceedings in Theoretical Computer Science, ISSN 2075-2180 ; 103
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-189990 (URN)10.4204/EPTCS.103.1 (DOI)
Conference
Workshop on Quantities in Formal Methods 2012
Projects
UPMARC
Available from: 2012-12-17 Created: 2013-01-06 Last updated: 2018-01-11Bibliographically approved
Abdulla, P. A., Atig, M. F. & Stenman, J. (2012). Dense-Timed Pushdown Automata. In: Proc. 27th ACM/IEEE Symposium on Logic in Computer Science: . Paper presented at 27th ACM/IEEE Symposium on Logic in Computer Science (LICS 2012), June 25-28, Dubrovnik, Croatia (pp. 35-44). IEEE Computer Society
Open this publication in new window or tab >>Dense-Timed Pushdown Automata
2012 (English)In: Proc. 27th ACM/IEEE Symposium on Logic in Computer Science, IEEE Computer Society, 2012, p. 35-44Conference paper, Published paper (Refereed)
Abstract [en]

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.

Place, publisher, year, edition, pages
IEEE Computer Society, 2012
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-184780 (URN)10.1109/LICS.2012.15 (DOI)000309059900009 ()978-0-7695-4769-5 (ISBN)
Conference
27th ACM/IEEE Symposium on Logic in Computer Science (LICS 2012), June 25-28, Dubrovnik, Croatia
Projects
UPMARC
Available from: 2012-11-13 Created: 2012-11-13 Last updated: 2018-01-12Bibliographically approved
Abdulla, P. A., Atig, M. F., Stenman, J. & Rezine, O. (2012). Multi-Pushdown Systems with Budgets. In: Formal Methods in Computer-Aided Design. Paper presented at FMCAD 2012 (pp. 24-33).
Open this publication in new window or tab >>Multi-Pushdown Systems with Budgets
2012 (English)In: Formal Methods in Computer-Aided Design, 2012, p. 24-33Conference paper, Published paper (Refereed)
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-189987 (URN)
Conference
FMCAD 2012
Projects
UPMARCConcurrent recursive programsProFun
Available from: 2013-01-06 Created: 2013-01-06 Last updated: 2018-01-11
Abdulla, P. A., Atig, M. F. & Stenman, J. (2012). The minimal cost reachability problem in priced timed pushdown systems. In: Language and Automata Theory and Applications: 6th International Conference, LATA 2012, A Coruña, Spain, March 5-9, 2012. Paper presented at LATA 2012, 6th International Conference on Language and Automata Theory and Applications; 5-9 Mar 2012; A Coruña, Spain (pp. 58-69). Berlin: Springer-Verlag
Open this publication in new window or tab >>The minimal cost reachability problem in priced timed pushdown systems
2012 (English)In: Language and Automata Theory and Applications: 6th International Conference, LATA 2012, A Coruña, Spain, March 5-9, 2012, Berlin: Springer-Verlag , 2012, p. 58-69Conference paper, Published paper (Refereed)
Place, publisher, year, edition, pages
Berlin: Springer-Verlag, 2012
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 7183
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-175086 (URN)10.1007/978-3-642-28332-1_6 (DOI)978-3-642-28331-4 (ISBN)
Conference
LATA 2012, 6th International Conference on Language and Automata Theory and Applications; 5-9 Mar 2012; A Coruña, Spain
Projects
UPMARC
Available from: 2012-02-29 Created: 2012-05-31 Last updated: 2018-01-12Bibliographically approved
Organisations

Search in DiVA

Show all publications