03968nam 2200589 a 450 991048503420332120200520144314.01-280-38884-697866135667683-642-15643-610.1007/978-3-642-15643-4(CKB)2670000000045082(SSID)ssj0000446325(PQKBManifestationID)11249867(PQKBTitleCode)TC0000446325(PQKBWorkID)10491643(PQKB)11571505(DE-He213)978-3-642-15643-4(MiAaPQ)EBC3065887(PPN)149024800(EXLCZ)99267000000004508220100728d2010 uy 0engurnn|008mamaatxtccrAutomated technology for verification and analysis 8th International Symposium, ATVA 2010, Singapore, September 21-24, 2010 : proceedings /Ahmed Bouajjani, Wei-Ngan Chin (eds.)1st ed. 2010.New York Springer20101 online resource (VIII, 404 p. 112 illus.) Lecture notes in computer science,0302-9743 ;6252LNCS sublibrary. SL 2, Programming and software engineeringBibliographic Level Mode of Issuance: Monograph3-642-15642-8 Includes bibliographical references and index.Invited 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.Lecture notes in computer science ;6252.LNCS sublibrary.SL 2,Programming and software engineering.Automatic theorem provingCongressesAutomatic theorem proving511.3/6028563Bouajjani Ahmed1759809Chin Wei-Ngan976690ATVA 2010MiAaPQMiAaPQMiAaPQBOOK9910485034203321Automated technology for verification and analysis4198462UNINA