03871nam 22006015 450 99646588440331620230405233849.010.1007/11537328(CKB)1000000000213174(SSID)ssj0000318970(PQKBManifestationID)11240032(PQKBTitleCode)TC0000318970(PQKBWorkID)10336290(PQKB)11318861(DE-He213)978-3-540-31899-6(MiAaPQ)EBC3067914(PPN)123096669(EXLCZ)99100000000021317420100723d2005 u| 0engurnn|008mamaatxtccrModel Checking Software[electronic resource] 12th International SPIN Workshop, San Francisco, CA, USA, August 22-24, 2005, Proceedings /edited by Patrick Godefroid1st ed. 2005.Berlin, Heidelberg :Springer Berlin Heidelberg :Imprint: Springer,2005.1 online resource (XII, 292 p.) Theoretical Computer Science and General Issues,2512-2029 ;3639Also available on the Internet.Printed edition: 9783540281955 Includes bibliographical references.Invited Talks/Papers -- Pushdown Model Checking for Security -- Execution Generated Test Cases: How to Make Systems Code Crash Itself -- Invited Tutorials -- Effective Bug Hunting with Spin and Modex -- The BLAST Software Verification System -- Model Checking Programs with Java PathFinder -- State Representation and Abstraction -- An Incremental Heap Canonicalization Algorithm -- Memory Efficient State Space Storage in Explicit Software Model Checking -- Counterexample-Based Refinement for a Boundedness Test for CFSM Languages -- Dealing with Concurrency -- Symbolic Model Checking for Asynchronous Boolean Programs -- Improving Spin’s Partial-Order Reduction for Breadth-First Search -- Sound Transaction-Based Reduction Without Cycle Detection -- Dealing with Complex Data -- Repairing Structurally Complex Data -- Crafting a Promela Front-End with Abstract Data Types to Mitigate the Sensitivity of (Compositional) Analysis to Implementation Choices -- Behavioural Models for Hierarchical Components -- Checking Temporal Properties -- On-the-Fly Emptiness Checks for Generalized Büchi Automata -- Stuttering Congruence for ? -- Verifying Pattern-Generated LTL Formulas: A Case Study -- Checking Security and Real-Time Properties -- Generic Verification of Security Protocols -- Using SPIN and Eclipse for Optimized High-Level Modeling and Analysis of Computer Network Attack Models -- Model Checking Machine Code with the GNU Debugger -- Tool Papers -- Etch: An Enhanced Type Checking Tool for Promela -- Enhanced Probabilistic Verification with 3Spin and 3Murphi -- SPLAT: A Tool for Model-Checking and Dynamically-Enforcing Abstractions -- Learning-Based Assume-Guarantee Verification (Tool Paper).Theoretical Computer Science and General Issues,2512-2029 ;3639Software engineeringCompilers (Computer programs)Computer scienceSoftware EngineeringCompilers and InterpretersComputer Science Logic and Foundations of ProgrammingSoftware engineering.Compilers (Computer programs).Computer science.Software Engineering.Compilers and Interpreters.Computer Science Logic and Foundations of Programming.005.1/4Godefroid Patrickedthttp://id.loc.gov/vocabulary/relators/edtLINK (Online service)BOOK996465884403316Model Checking Software771961UNISA01223nam0 22002891i 450 UON0031749020231205104125.66497-377-8408-120081121d2006 |0itac50 barumFRERO|||| 1||||Eugeniu Neculcea Un diplomat regăsitUn diplomate retrouvé Editie ingrijita si studiu introductiv deEdition soignée et étude introductive par Marcela SălăgeanCluj-NapocaInstitutul Cultural Român2006IX-LXXV, 83 p.tav.30 cm.NECULCEA EUGENIUUONC069860FIRomaniaStoriaUONC042197FICluj-NapocaUONL003746949.8Storia della Romania21SĂLĂGEANMarcelaUONV181136Institutul Cultural Român. Centrul de Studii TransilvaneUONV274812650ITSOL20250801RICASIBA - SISTEMA BIBLIOTECARIO DI ATENEOUONSIUON00317490SIBA - SISTEMA BIBLIOTECARIO DI ATENEOSI EO DUOMO XVI 0064 SI EO 41074 5 0064 Eugeniu Neculcea1374516UNIOR