liu.seSearch for publications in DiVA
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Abstracting and Counting Synchronizing Processes
Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, The Institute of Technology. (ESLAB)
Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, The Institute of Technology.
Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, The Institute of Technology.
Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, The Institute of Technology.
2015 (English)In: Verification, Model Checking, and Abstract Interpretation: 16th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2015), Mumbai, India, Jan. 12-14, 2015., Springer, 2015, 227-244 p.Conference paper, Published paper (Refereed)
Abstract [en]

We address the problem of automatically establishing synchronization dependent correctness (e.g. due to using barriers or ensuring absence of deadlocks) of programs generating an arbitrary number of concurrent processes and manipulating variables ranging over an infinite domain. Automatically checking such properties for these programs is beyond the capabilities of current verification techniques. For this purpose, we describe an original logic that mixes two sorts of variables: those shared and manipulated by the concurrent processes, and ghost variables referring to the number of processes satisfying predicates on shared and local program variables. We then combine existing works on counter, predicate, and constrained monotonic abstraction and nest two cooperating counter example based refinement loops for establishing correctness (safety expressed as non reachability of configurations satisfying formulas in our logic). We have implemented a tool (Pacman, for predicated constrained monotonic abstraction) and used it to perform parameterized verification for several programs whose correctness crucially depends on precisely capturing the number of synchronizing processes.

Place, publisher, year, edition, pages
Springer, 2015. 227-244 p.
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 8931
National Category
Computer and Information Science
Identifiers
URN: urn:nbn:se:liu:diva-114467DOI: 10.1007/978-3-662-46081-8_13ISI: 000354784200013ISBN: 978-3-662-46080-1 (print)ISBN: 978-3-662-46081-8 (print)OAI: oai:DiVA.org:liu-114467DiVA: diva2:789929
Conference
VMCAI 15
Available from: 2015-02-20 Created: 2015-02-20 Last updated: 2015-06-12

Open Access in DiVA

No full text

Other links

Publisher's full text

Authority records BETA

Ganjei, ZeinabRezine, AhmedIon Eles, PetruPeng, Zebo

Search in DiVA

By author/editor
Ganjei, ZeinabRezine, AhmedIon Eles, PetruPeng, Zebo
By organisation
Software and SystemsThe Institute of Technology
Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 165 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf