Loading...
Please wait, while we are loading the content...
Similar Documents
Constraint-based automatic verification of abstract models of multithreaded programs
| Content Provider | Scilit |
|---|---|
| Author | Delzanno, Giorgio |
| Copyright Year | 2007 |
| Description | We present a technique for the automated verification of abstract models of multithreaded programs providing fresh name generation, name mobility, and unbounded control. As high level specification language we adopt here an extension of communication finite-state machines with local variables ranging over an infinite name domain, called TDL programs. Communication machines have been proved very effective for representing communication protocols as well as for representing abstractions of multithreaded software. The verification method that we propose is based on the encoding of TDL programs into a low level language based on multiset rewriting and constraints that can be viewed as an extension of Petri Nets. By means of this encoding, the symbolic verification procedure developed for the low level language in our previous work can now be applied to TDL programs. Furthermore, the encoding allows us to isolate a decidable class of verification problems for TDL programs that still provide fresh name generation, name mobility, and unbounded control. Our syntactic restrictions are in fact defined on the internal structure of threads: In order to obtain a complete and terminating method, threads are only allowed to have at most one local variable (ranging over an infinite domain of names). |
| Related Links | http://arxiv.org/pdf/cs/0601038 https://www.cambridge.org/core/services/aop-cambridge-core/content/view/C74D6CA3663E5712808E97C60C1C359B/S1471068406002821a.pdf/div-class-title-constraint-based-automatic-verification-of-abstract-models-of-multithreaded-programs-div.pdf |
| Ending Page | 91 |
| Page Count | 25 |
| Starting Page | 67 |
| ISSN | 14710684 |
| e-ISSN | 14753081 |
| DOI | 10.1017/s1471068406002821 |
| Journal | Theory and Practice of Logic Programming |
| Issue Number | 1-2 |
| Volume Number | 7 |
| Language | English |
| Publisher | Cambridge University Press (CUP) |
| Publisher Date | 2007-01-01 |
| Access Restriction | Open |
| Subject Keyword | Theory and Practice of Logic Programming Hardware and Architecture Multithreaded Programs |
| Content Type | Text |
| Resource Type | Article |
| Subject | Artificial Intelligence Theoretical Computer Science Computational Theory and Mathematics Hardware and Architecture Software |
