LEADER 06479nam 22008055 450 001 9910485034203321 005 20251226195843.0 010 $a1-280-38884-6 010 $a9786613566768 010 $a3-642-15643-6 024 7 $a10.1007/978-3-642-15643-4 035 $a(CKB)2670000000045082 035 $a(SSID)ssj0000446325 035 $a(PQKBManifestationID)11249867 035 $a(PQKBTitleCode)TC0000446325 035 $a(PQKBWorkID)10491643 035 $a(PQKB)11571505 035 $a(DE-He213)978-3-642-15643-4 035 $a(MiAaPQ)EBC3065887 035 $a(PPN)149024800 035 $a(BIP)32170374 035 $a(EXLCZ)992670000000045082 100 $a20100920d2010 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aAutomated Technology for Verification and Analysis $e8th International Symposium, ATVA 2010, Singapore, September 21-24, 2010, Proceedings /$fedited by Ahmed Bouajjani, Wei-Ngan Chin 205 $a1st ed. 2010. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2010. 215 $a1 online resource (VIII, 404 p. 112 illus.) 225 1 $aProgramming and Software Engineering,$x2945-9168 ;$v6252 300 $aBibliographic Level Mode of Issuance: Monograph 311 08$a3-642-15642-8 320 $aIncludes bibliographical references and index. 327 $aInvited Talks -- Probabilistic Automata on Infinite Words: Decidability and Undecidability Results -- Abstraction Learning -- Synthesis: Words and Traces -- Regular Papers -- Promptness in ?-Regular Automata -- Using Redundant Constraints for Refinement -- Methods for Knowledge Based Controlling of Distributed Systems -- Composing Reachability Analyses of Hybrid Systems for Safety and Stability -- The Complexity of Codiagnosability for Discrete Event and Timed Systems -- On Scenario Synchronization -- Compositional Algorithms for LTL Synthesis -- What?s Decidable about Sequences? -- A Study of the Convergence of Steady State Probabilities in a Closed Fork-Join Network -- Lattice-Valued Binary Decision Diagrams -- A Specification Logic for Exceptions and Beyond -- Non-monotonic Refinement of Control Abstraction for Concurrent Programs -- An Approach for Class Testing from Class Contracts -- Efficient On-the-Fly Emptiness Check for Timed Büchi Automata -- Reachability as Derivability, Finite Countermodels and Verification -- LTL Can Be More Succinct -- Automatic Generation of History-Based Access Control from Information Flow Specification -- Auxiliary Constructs for Proving Liveness in Compassion Discrete Systems -- Symbolic Unfolding of Parametric Stopwatch Petri Nets -- Recursive Timed Automata -- Probabilistic Contracts for Component-Based Design -- Tool Papers -- Model-Checking Web Applications with Web-TLR -- GAVS: Game Arena Visualization and Synthesis -- CRI: Symbolic Debugger for MCAPI Applications -- MCGP: A Software Synthesis Tool Based on Model Checking and Genetic Programming -- ECDAR: An Environment for Compositional Design and Analysis of Real Time Systems -- Developing Model Checkers Using PAT -- YAGA: Automated Analysis of Quantitative Safety Specifications in Probabilistic B.-COMBINE: A Tool on Combined Formal Methods for Bindingly Verification -- Rbminer: A Tool for Discovering Petri Nets from Transition Systems. 330 $aThese proceedings contain the papers presented at the 8th Internationl S- posium on Automated Technology for Veri'cation and Analysis held during September 21-24, 2010 in Singapore. The primary objective of the ATVA c- ferences remains the same: to exchange and promote the latest advances of state-of-the-art research on theoretical and practical aspects of automated an- ysis, veri'cation and synthesis. From 72 papers submitted to ATVA 2010 in response to our call for papers, the Program Committee accepted 21 regular papers and 9 tool papers. Each paper received at least three reviews. The Program Committee worked hard to ensure that every submission received a rigorous and fair evaluation, with the ?nalprogramselectedaftera10-dayonlinediscussionsviatheEasychairsystem. OurprogramalsoincludedthreekeynotetalksandinvitedtutorialsbyThomas A.Henzinger(ISTAustria),JoxanJa'ar(NationalUniversityofSingapore)and IgorWalukiewicz(CNRS, France).Theconferenceorganizersweretrulygrateful to have such distinguished researchers as keynote speakers for the symposium. A new feature for the ATVA symposium this year were the two co-located workshops, In'nity 2010 (co-chaired by Yu-Fang Chen and Ahmed Rezine) and PMCW 2010 (co-chaired by Jun Sun and Hai Wang). We are delighted with the expanded scope, interactions and depth that the two workshops helped bring to the symposium. Many people worked hard and o'ered their valuable time so generously to make ATVA 2010 successful. First and foremost, we would like to thank all authors who worked hard to complete and submit papers to the conference. The ProgramCommittee members, reviewersand Steering Committee members alsodeservespecialrecognition.Without them, a competitive andpeer-reviewed international symposium simply cannot take place. 410 0$aProgramming and Software Engineering,$x2945-9168 ;$v6252 606 $aSoftware engineering 606 $aComputer programming 606 $aComputer networks 606 $aComputer science 606 $aCompilers (Computer programs) 606 $aSoftware Engineering 606 $aProgramming Techniques 606 $aComputer Communication Networks 606 $aComputer Science Logic and Foundations of Programming 606 $aCompilers and Interpreters 615 0$aSoftware engineering. 615 0$aComputer programming. 615 0$aComputer networks. 615 0$aComputer science. 615 0$aCompilers (Computer programs) 615 14$aSoftware Engineering. 615 24$aProgramming Techniques. 615 24$aComputer Communication Networks. 615 24$aComputer Science Logic and Foundations of Programming. 615 24$aCompilers and Interpreters. 676 $a511.3/6028563 701 $aBouajjani$b Ahmed$01759809 701 $aChin$b Wei-Ngan$0976690 712 12$aATVA 2010 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910485034203321 996 $aAutomated technology for verification and analysis$94198462 997 $aUNINA