Treffer: Model checking multithreaded programs with asynchronous atomic methods

Title:
Model checking multithreaded programs with asynchronous atomic methods
Authors:
SEN, Koushik, VISWANATHAN, Mahesh
Source:
Computer aided verification (18th international conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006)0CAV 2006. :300-314
Publisher Information:
Berlin; New York: Springer, 2006.
Publication Year:
2006
Physical Description:
print, 32 ref 1
Original Material:
INIST-CNRS
Subject Terms:
Computer science, Informatique, Sciences exactes et technologie, Exact sciences and technology, Sciences appliquees, Applied sciences, Informatique; automatique theorique; systemes, Computer science; control theory; systems, Logiciel, Software, Génie logiciel, Software engineering, Atteignabilité, Reachability, Asequibilidad, Décidabilité, Decidability, Decidibilidad, Langage JAVA, JAVA language, Lenguaje JAVA, Langage programmation, Programming language, Lenguaje programación, Machine état fini, Finite state machine, Máquina estado finito, Multitâche, Multithread, Multitarea, Métamodèle, Metamodel, Metamodelo, Méthode raffinement, Refinement method, Método afinamiento, Programme contrôle, Checking program, Programa control, Réutilisation, Reuse, Reutilización, Vérification modèle, Model checking, Verificación modelo, Vérification programme, Program verification, Verificación programa, Patron conception, Design pattern, Patrón Concepción
Document Type:
Konferenz Conference Paper
File Description:
text
Language:
English
Author Affiliations:
Department of Computer Science, University of Illinois at Urbana-Champaign, United States
ISSN:
0302-9743
Access URL:
http://pascal-francis.inist.fr/vibad/index.php?action=search&terms=19150363
Rights:
Copyright 2007 INIST-CNRS
CC BY 4.0
Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS
Notes:
Computer science; theoretical automation; systems
Accession Number:
edscal.19150363
Database:
PASCAL Archive

Weitere Informationen

In order to make multithreaded programming manageable, programmers often follow a design principle where they break the problem into tasks which are then solved asynchronously and concurrently on different threads. This paper investigates the problem of model checking programs that follow this idiom. We present a programming language SPL that encapsulates this design pattern. SPL extends simplified form of sequential Java to which we add the capability of making asynchronous method invocations in addition to the standard synchronous method calls and the ability to execute asynchronous methods in threads atomically and concurrently. Our main result shows that the control state reachability problem for finite SPL programs is decidable. Therefore, such multithreaded programs can be model checked using the counterexample guided ion-refinement framework.