Sökning: WFRF:(Ganjei Zeinab)
> (2014) >
Abstracting and Cou...
Abstracting and Counting Synchronizing Processes
-
- Ganjei, Zeinab (författare)
- Linköpings universitet,Programvara och system,Tekniska högskolan,ESLAB
-
- Rezine, Ahmed (författare)
- Linköpings universitet,Programvara och system,ESLAB
-
- Eles, Petru (författare)
- Linköpings universitet,Programvara och system,Tekniska högskolan,ESLAB
-
visa fler...
-
- Peng, Zebo (författare)
- Linköpings universitet,Programvara och system,Tekniska högskolan,ESLAB
-
visa färre...
-
(creator_code:org_t)
- 2014
- Engelska 35 s.
-
Serie: Technical reports in Computer and Information Science, 1654-7233
- Relaterad länk:
-
https://liu.diva-por... (primary) (Raw object)
-
visa fler...
-
https://urn.kb.se/re...
-
visa färre...
Abstract
Ämnesord
Stäng
- 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.
Nyckelord
- Parameterized verification
- counting logic
- barrier synchronization
- deadlock freedom
- multithreaded programs
- counter abstraction
- predicate abstraction
- constrained monotonic abstraction
Publikations- och innehållstyp
- vet (ämneskategori)
- rap (ämneskategori)