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. (ESLAB)
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. (ESLAB)
2014 (English)Report (Other academic)
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 refering 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
2014. , 35 p.
Series
Technical reports in Computer and Information Science, ISSN 1654-7233
Keyword [en]
Parameterized verification, counting logic, barrier synchronization, deadlock freedom, multithreaded programs, counter abstraction, predicate abstraction, constrained monotonic abstraction
National Category
Engineering and Technology
Identifiers
URN: urn:nbn:se:liu:diva-111739OAI: oai:DiVA.org:liu-111739DiVA: diva2:759689
Available from: 2014-10-30 Created: 2014-10-30 Last updated: 2014-10-31Bibliographically approved

Open Access in DiVA

fulltext(654 kB)101 downloads
File information
File name FULLTEXT01.pdfFile size 654 kBChecksum SHA-512
b07438142714975f0655b4e2a88e2b37f1b4ea25a25427dbab219b6966e0672ab2f98b79e1402deee2ac579588877839cee740e86d74861868aa8e92abd6a2d1
Type fulltextMimetype application/pdf

Authority records BETA

Ganjei, ZeinabRezine, AhmedEles, PetruPeng, Zebo

Search in DiVA

By author/editor
Ganjei, ZeinabRezine, AhmedEles, PetruPeng, Zebo
By organisation
Software and SystemsThe Institute of Technology
Engineering and Technology

Search outside of DiVA

GoogleGoogle Scholar
Total: 101 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

urn-nbn

Altmetric score

urn-nbn
Total: 233 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