Data Portal @ linkeddatafragments.org

Matches in Harvard for { <http://id.lib.harvard.edu/aleph/008529125/catalog> ?p ?o. }

• catalog abstract "The SPIN workshop is a forum for researchers interested in the subject of automata-based, explicit-state model checking technologies for the analysis and veri?cation of asynchronous concurrent and distributed systems. The SPIN - del checker (http://netlib.bell-labs.com/netlib/spin/whatispin.html), developed by Gerard Holzmann, is one of the best known systems of this kind, and has attracted a large user community. This can likely be attributed to its e?cient state exploration algorithms. The fact that SPIN’s modeling language, Promela, resembles a programming language has probably also contributed to its success. Traditionally, the SPIN workshops present papers on extensions and uses of SPIN. As an experiment, this year’s workshop was broadened to have a slightly wider focus than previous workshops in that papers on software veri?cation were encouraged. Consequently, a small collection of papers describe attempts to analyze and verify programs written in conventional programming languages. Solutions include translations from source code to Promela, as well as specially designed model checkers that accept source code. We believe that this is an - teresting research direction for the formal methods community, and that it will result in a new set of challenges and solutions. Of course, abstraction becomes the key solution to deal with very large state spaces. However, we also see - tential for integrating model checking with techniques such as static program analysis and testing. Papers on these issues have therefore been included in the proceedings.".
• catalog contributor b11931738.
• catalog contributor b11931739.
• catalog contributor b11931740.
• catalog contributor b11931741.
• catalog created "2000.".
• catalog date "2000".
• catalog date "2000.".
• catalog dateCopyrighted "2000.".
• catalog description "Includes bibliographical references and index.".
• catalog description "Symmetric Spin / Dragan Bosnacki, Dennis Dams and Leszek Holenderski -- Using Garbage Collection in Model Checking / Radu Iosif and Riccardo Sisto -- Model Checking Based on Simultaneous Reachability Analysis / Bengi Karacali and Kuo-Chung Tai -- Testing Spin's LTL Formula Conversion into Buchi Automata with Randomly Generated Input / Heikki Tauriainen and Keijo Heljanko -- Verification and Optimization of a PLC Control Schedule / Ed Brinksma and Angelika Mader -- Modeling the ASCB-D Synchronization Algorithm with SPIN: A Case Study / Nicholas Weininger and Darren Cofer -- Bebop: A Symbolic Model Checker for Boolean Programs / Thomas Ball and Sriram K. Rajamani -- Logic Verification of ANSI-C Code with SPIN / Gerard J. Holzmann -- Interaction Abstraction for Compositional Finite State Systems / Wayne Liu -- Correctness by Construction: Towards Verification in Hierarchical System Development / Mila Majster-Cederbaum and Frank Salger -- Linking STeP with SPIN / Anca Browne, Henny Sipma and Ting Zhang.".
• catalog description "The SPIN workshop is a forum for researchers interested in the subject of automata-based, explicit-state model checking technologies for the analysis and veri?cation of asynchronous concurrent and distributed systems. The SPIN - del checker (http://netlib.bell-labs.com/netlib/spin/whatispin.html), developed by Gerard Holzmann, is one of the best known systems of this kind, and has attracted a large user community. This can likely be attributed to its e?cient state exploration algorithms. The fact that SPIN’s modeling language, Promela, resembles a programming language has probably also contributed to its success. Traditionally, the SPIN workshops present papers on extensions and uses of SPIN. As an experiment, this year’s workshop was broadened to have a slightly wider focus than previous workshops in that papers on software veri?cation were encouraged. Consequently, a small collection of papers describe attempts to analyze and verify programs written in conventional programming languages. Solutions include translations from source code to Promela, as well as specially designed model checkers that accept source code. We believe that this is an - teresting research direction for the formal methods community, and that it will result in a new set of challenges and solutions. Of course, abstraction becomes the key solution to deal with very large state spaces. However, we also see - tential for integrating model checking with techniques such as static program analysis and testing. Papers on these issues have therefore been included in the proceedings.".
• catalog extent "x, 342 p. :".
• catalog identifier "3540410309 (softcover : alk. paper)".
• catalog isPartOf "Lecture notes in computer science ; 1885".
• catalog issued "2000".
• catalog issued "2000.".
• catalog language "eng".
• catalog publisher "Berlin ; New York : Springer,".
• catalog subject "005.2/76 21".
• catalog subject "Computer science.".
• catalog subject "Computer simulation Testing Data processing Congresses.".
• catalog subject "Computer software Verification Congresses.".
• catalog subject "Logic design.".
• catalog subject "QA76.76.V47 I58 2000".
• catalog subject "SPIN (Computer file) Congresses.".
• catalog subject "Software engineering.".
• catalog tableOfContents "Symmetric Spin / Dragan Bosnacki, Dennis Dams and Leszek Holenderski -- Using Garbage Collection in Model Checking / Radu Iosif and Riccardo Sisto -- Model Checking Based on Simultaneous Reachability Analysis / Bengi Karacali and Kuo-Chung Tai -- Testing Spin's LTL Formula Conversion into Buchi Automata with Randomly Generated Input / Heikki Tauriainen and Keijo Heljanko -- Verification and Optimization of a PLC Control Schedule / Ed Brinksma and Angelika Mader -- Modeling the ASCB-D Synchronization Algorithm with SPIN: A Case Study / Nicholas Weininger and Darren Cofer -- Bebop: A Symbolic Model Checker for Boolean Programs / Thomas Ball and Sriram K. Rajamani -- Logic Verification of ANSI-C Code with SPIN / Gerard J. Holzmann -- Interaction Abstraction for Compositional Finite State Systems / Wayne Liu -- Correctness by Construction: Towards Verification in Hierarchical System Development / Mila Majster-Cederbaum and Frank Salger -- Linking STeP with SPIN / Anca Browne, Henny Sipma and Ting Zhang.".
• catalog title "SPIN model checking and software verification : 7th International SPIN Workshop, Stanford, CA, USA, August 30-September 1, 2000 : proceedings / Klaus Havelund, John Penix, Willem Visser (eds.).".
• catalog type "Conference proceedings. fast".
• catalog type "Stanford (Calif., 2000) swd".
• catalog type "text".