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

Direct link
BETA
Cederberg, Jonathan
Publications (6 of 6) Show all publications
Abdulla, P. A., Atig, M. F., Cederberg, J., Modi, S., Rezine, O. & Saini, G. (2015). MPass: An efficient tool for the analysis of message-passing programs. In: Formal Aspects of Component Software: . Paper presented at FACS 2014, September 10–12, Bertinoro, Italy (pp. 198-206). Springer
Open this publication in new window or tab >>MPass: An efficient tool for the analysis of message-passing programs
Show others...
2015 (English)In: Formal Aspects of Component Software, Springer, 2015, p. 198-206Conference paper, Published paper (Refereed)
Place, publisher, year, edition, pages
Springer, 2015
Series
Lecture Notes in Computer Science ; 8997
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-237847 (URN)10.1007/978-3-319-15317-9_13 (DOI)978-3-319-15316-2 (ISBN)
Conference
FACS 2014, September 10–12, Bertinoro, Italy
Projects
ProFuNUPMARC
Available from: 2015-01-30 Created: 2014-12-05 Last updated: 2018-01-11Bibliographically approved
Abdulla, P. A., Atig, M. F. & Cederberg, J. (2013). Analysis of message passing programs using SMT-solvers. In: Automated Technology for Verification and Analysis: ATVA 2013. Paper presented at ATVA 2013, October 15-18, Hanoi, Vietnam (pp. 272-286). Springer Berlin/Heidelberg
Open this publication in new window or tab >>Analysis of message passing programs using SMT-solvers
2013 (English)In: Automated Technology for Verification and Analysis: ATVA 2013, Springer Berlin/Heidelberg, 2013, p. 272-286Conference paper, Published paper (Refereed)
Place, publisher, year, edition, pages
Springer Berlin/Heidelberg, 2013
Series
Lecture Notes in Computer Science ; 8172
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-213239 (URN)10.1007/978-3-319-02444-8_20 (DOI)978-3-319-02443-1 (ISBN)
Conference
ATVA 2013, October 15-18, Hanoi, Vietnam
Projects
UPMARCConcurrent recusive programs
Available from: 2013-12-19 Created: 2013-12-19 Last updated: 2018-01-11Bibliographically approved
Abdulla, P. A., Cederberg, J. & Vojnar, T. (2013). Monotonic abstraction for programs with multiply-linked structures. International Journal of Foundations of Computer Science, 24(2), 187-210
Open this publication in new window or tab >>Monotonic abstraction for programs with multiply-linked structures
2013 (English)In: International Journal of Foundations of Computer Science, ISSN 0129-0541, Vol. 24, no 2, p. 187-210Article in journal (Refereed) Published
Abstract [en]

We investigate the use of monotonic abstraction and backward reachability analysis as means of performing shape analysis on programs with multiply pointed structures. By encoding the heap as a vertex- and edge-labeled graph, we can model the low level behaviour exhibited by programs written in the C programming language. Using the notion of signatures, which are predicates that define sets of heaps, we can check properties such as absence of null pointer dereference and shape invariants. We report on the results from running a prototype based on the method on several programs such as insertion into and merging of doubly-linked lists.

National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-190238 (URN)10.1142/S0129054113400078 (DOI)000319838100003 ()
Projects
UPMARC
Funder
Swedish Research Council
Available from: 2013-01-08 Created: 2013-01-07 Last updated: 2018-01-11Bibliographically approved
Abdulla, P. A., Atig, M. F. & Cederberg, J. (2012). Timed lossy channel systems. In: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science: FSTTCS 2012. Paper presented at FSTTCS 2012 (pp. 374-386). Dagstuhl, Germany: Leibniz-Zentrum für Informatik
Open this publication in new window or tab >>Timed lossy channel systems
2012 (English)In: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science: FSTTCS 2012, Dagstuhl, Germany: Leibniz-Zentrum für Informatik , 2012, p. 374-386Conference paper, Published paper (Refereed)
Place, publisher, year, edition, pages
Dagstuhl, Germany: Leibniz-Zentrum für Informatik, 2012
Series
Leibniz International Proceedings in Informatics ; 18
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-189985 (URN)10.4230/LIPIcs.FSTTCS.2012.374 (DOI)978-3-939897-47-7 (ISBN)
Conference
FSTTCS 2012
Projects
UPMARC
Available from: 2012-12-10 Created: 2013-01-06 Last updated: 2018-01-11Bibliographically approved
Abdulla, P. A., Cederberg, J. & Kaati, L. (2010). Analyzing the security in the GSM radio network using attack jungles. In: Leveraging Applications of Formal Methods, Verification, and Validation: Part I. Paper presented at 4th International Symposium on Leveraging Applications, Heraklion, Greece, October 18-21, 2010 (pp. 60-74). Berlin: Springer-Verlag
Open this publication in new window or tab >>Analyzing the security in the GSM radio network using attack jungles
2010 (English)In: Leveraging Applications of Formal Methods, Verification, and Validation: Part I, Berlin: Springer-Verlag , 2010, p. 60-74Conference paper, Published paper (Refereed)
Place, publisher, year, edition, pages
Berlin: Springer-Verlag, 2010
Series
Lecture Notes in Computer Science ; 6415
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-152913 (URN)10.1007/978-3-642-16558-0_8 (DOI)000289493100008 ()978-3-642-16557-3 (ISBN)
Conference
4th International Symposium on Leveraging Applications, Heraklion, Greece, October 18-21, 2010
Available from: 2011-05-03 Created: 2011-05-03 Last updated: 2018-01-12Bibliographically approved
Abdulla, P. A., Bouajjani, A., Cederberg, J., Haziza, F. & Rezine, A. (2008). Monotonic abstraction for programs with dynamic memory heaps. In: Gupta A, Malik S (Ed.), Computer Aided Verification. Paper presented at 20th International Conference on Computer Aided Verification Princeton, NJ, JUL 07, 2008 (pp. 341-354). Berlin: Springer-Verlag
Open this publication in new window or tab >>Monotonic abstraction for programs with dynamic memory heaps
Show others...
2008 (English)In: Computer Aided Verification / [ed] Gupta A, Malik S, Berlin: Springer-Verlag , 2008, p. 341-354Conference paper, Published paper (Refereed)
Abstract [en]

We propose a new approach for automatic verification of programs with dynamic heap manipulation. The method is based on symbolic (backward) reachability analysis using upward-closed sets of heaps w.r.t. an appropriate preorder on graphs. These sets are represented by a finite set of minimal graph patterns corresponding to a set of bad configurations. We define an abstract semantics for the programs which is monotonic w.r.t. the preorder. Moreover, we prove that our analysis always terminates by showing that the preorder is a well-quasi ordering. Our results are presented for the case of programs with 1-next selector. We provide experimental results showing the effectiveness of our approach.

Place, publisher, year, edition, pages
Berlin: Springer-Verlag, 2008
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 5123
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-106059 (URN)10.1007/978-3-540-70545-1_33 (DOI)000257539900033 ()
Conference
20th International Conference on Computer Aided Verification Princeton, NJ, JUL 07, 2008
Available from: 2009-06-13 Created: 2009-06-13 Last updated: 2018-01-13Bibliographically approved
Organisations

Search in DiVA

Show all publications