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

Direct link
BETA
Trinh, Cong Quy
Publications (4 of 4) Show all publications
Abdulla, P. A., Jonsson, B. & Trinh, C. Q. (2018). Fragment abstraction for concurrent shape analysis. In: Programming Languages and Systems: . Paper presented at ESOP 2018 (pp. 442-471). Springer
Open this publication in new window or tab >>Fragment abstraction for concurrent shape analysis
2018 (English)In: Programming Languages and Systems, Springer, 2018, p. 442-471Conference paper, Published paper (Refereed)
Place, publisher, year, edition, pages
Springer, 2018
Series
Lecture Notes in Computer Science ; 10801
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-368505 (URN)10.1007/978-3-319-89884-1_16 (DOI)978-3-319-89883-4 (ISBN)
Conference
ESOP 2018
Projects
UPMARC
Available from: 2018-04-14 Created: 2018-12-05 Last updated: 2018-12-07Bibliographically approved
Abdulla, P., Jonsson, B. & Trinh, C. Q. (2016). Automated Verification of Linearization Policies. In: Automated Verification of Linearization Policies: 23rd International Symposium, SAS 2016, Edinburgh, UK, September 8-10, 2016, Proceedings. Paper presented at 23rd International Symposium, SAS 2016.
Open this publication in new window or tab >>Automated Verification of Linearization Policies
2016 (English)In: Automated Verification of Linearization Policies: 23rd International Symposium, SAS 2016, Edinburgh, UK, September 8-10, 2016, Proceedings, 2016Conference paper, Published paper (Other academic)
Abstract [en]

We present a novel framework for automated verification of linearizability for concurrent data structures that implement sets, stacks, and queues. The framework requires the user to provide a linearization policy, which describes how linearization point placement in different concurrent threads affect each other; such linearization policies are often provided informally together with descriptions of new algorithms. We present a specification formalism for linearization policies which allows the user to specify, in a simple and concise manner, complex patterns including non-fixed linearization points. To automate verification, we extend thread-modular reasoning to bound the number of considered threads, and use a novel symbolic representation for unbounded heap structures that store data from an unbounded domain. We have implemented our framework in a tool and successfully used it to prove linearizability for a wide range of algorithms, including all implementations of concurrent sets, stacks, and queues based on singly-linked lists that are known to us from the literature.

National Category
Computer Systems
Research subject
Computer Science
Identifiers
urn:nbn:se:uu:diva-305226 (URN)10.1007/978-3-662-53413-7_4 (DOI)000388924600004 ()9783662534120 (ISBN)9783662534137 (ISBN)
Conference
23rd International Symposium, SAS 2016
Available from: 2016-10-13 Created: 2016-10-13 Last updated: 2017-01-02Bibliographically approved
Abdulla, P. A., Holík, L., Jonsson, B., Lengál, O., Trinh, C. Q. & Vojnar, T. (2016). Verification of heap manipulating programs with ordered data by extended forest automata. Acta Informatica, 53(4), 357-385
Open this publication in new window or tab >>Verification of heap manipulating programs with ordered data by extended forest automata
Show others...
2016 (English)In: Acta Informatica, ISSN 0001-5903, E-ISSN 1432-0525, Vol. 53, no 4, p. 357-385Article in journal (Refereed) Published
Abstract [en]

We present a general framework for verifying programs with complex dynamic linked data structures whose correctness depends on ordering relations between stored data values. The underlying formalism of our framework is that of forest automata (FA), which has previously been developed for verification of heap-manipulating programs. We extend FA with constraints between data elements associated with nodes of the heaps represented by FA, and we present extended versions of all operations needed for using the extended FA in a fully-automated verification approach, based on abstract interpretation. We have implemented our approach as an extension of the Forester tool and successfully applied it to a number of programs dealing with data structures such as various forms of singly- and doubly-linked lists, binary search trees, as well as skip lists.

National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-295451 (URN)10.1007/s00236-015-0235-0 (DOI)000376978100003 ()
Projects
ProFuNUPMARC
Funder
Swedish Foundation for Strategic Research
Available from: 2015-05-07 Created: 2016-06-07 Last updated: 2018-01-10Bibliographically approved
Abdulla, P. A., Holík, L., Jonsson, B., Lengál, O., Trinh, C. Q. & Vojnar, T. (2013). Verification of heap manipulating programs with ordered data by extended forest automata. In: Automated Technology for Verification and Analysis: ATVA 2013. Paper presented at ATVA 2013, October 15-18, Hanoi, Vietnam (pp. 224-239). Springer Berlin/Heidelberg
Open this publication in new window or tab >>Verification of heap manipulating programs with ordered data by extended forest automata
Show others...
2013 (English)In: Automated Technology for Verification and Analysis: ATVA 2013, Springer Berlin/Heidelberg, 2013, p. 224-239Conference paper, Published paper (Refereed)
Place, publisher, year, edition, pages
Springer Berlin/Heidelberg, 2013
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 8172
National Category
Computer Sciences
Research subject
Computer Science
Identifiers
urn:nbn:se:uu:diva-212135 (URN)10.1007/978-3-319-02444-8_17 (DOI)978-3-319-02443-1 (ISBN)
Conference
ATVA 2013, October 15-18, Hanoi, Vietnam
Projects
ProFuNUPMARC
Funder
Swedish Foundation for Strategic Research
Available from: 2013-12-06 Created: 2013-12-06 Last updated: 2018-01-11Bibliographically approved
Organisations

Search in DiVA

Show all publications