05933nam 22007935 450 99646572470331620200629203507.03-540-27813-310.1007/b98490(CKB)1000000000212451(SSID)ssj0000127767(PQKBManifestationID)11141130(PQKBTitleCode)TC0000127767(PQKBWorkID)10062561(PQKB)10961635(DE-He213)978-3-540-27813-9(MiAaPQ)EBC3088566(PPN)155165216(EXLCZ)99100000000021245120121227d2004 u| 0engurnn#008mamaatxtccrComputer Aided Verification[electronic resource] 16th International Conference, CAV 2004, Boston, MA, USA, July 13-17, 2004, Proceedings /edited by Rajeev Alur, Doron A. Peled1st ed. 2004.Berlin, Heidelberg :Springer Berlin Heidelberg :Imprint: Springer,2004.1 online resource (XII, 536 p.)Lecture Notes in Computer Science,0302-9743 ;3114Bibliographic Level Mode of Issuance: Monograph3-540-22342-8 Includes bibliographical references at the end of each chapters and index.Rob Tristan Gerth: 1956–2003 -- Static Program Analysis via 3-Valued Logic -- Deductive Verification of Pipelined Machines Using First-Order Quantification -- A Formal Reduction for Lock-Free Parallel Algorithms -- An Efficiently Checkable, Proof-Based Formulation of Vacuity in Model Checking -- Termination of Linear Programs -- Symbolic Model Checking of Non-regular Properties -- Proving More Properties with Bounded Model Checking -- Parallel LTL-X Model Checking of High-Level Petri Nets Based on Unfoldings -- Using Interface Refinement to Integrate Formal Verification into the Design Cycle -- Indexed Predicate Discovery for Unbounded System Verification -- Range Allocation for Separation Logic -- An Experimental Evaluation of Ground Decision Procedures -- DPLL(T): Fast Decision Procedures -- Verifying ?-Regular Properties of Markov Chains -- Statistical Model Checking of Black-Box Probabilistic Systems -- Compositional Specification and Model Checking in GSTE -- GSTE Is Partitioned Model Checking -- Stuck-Free Conformance -- Symbolic Simulation, Model Checking and Abstraction with Partially Ordered Boolean Functional Vectors -- Functional Dependency for Verification Reduction -- Verification via Structure Simulation -- Symbolic Parametric Safety Analysis of Linear Hybrid Systems with BDD-Like Data-Structures -- Abstraction-Based Satisfiability Solving of Presburger Arithmetic -- Widening Arithmetic Automata -- Why Model Checking Can Improve WCET Analysis -- Regular Model Checking for LTL(MSO) -- Image Computation in Infinite State Model Checking -- Abstract Regular Model Checking -- Global Model-Checking of Infinite-State Systems -- QB or Not QB: An Efficient Execution Verification Tool for Memory Orderings -- Verification of an Advanced mips-Type Out-of-Order Execution Algorithm -- Automatic Verification of Sequential Consistency for Unbounded Addresses and Data Values -- Efficient Modeling of Embedded Memories in Bounded Model Checking -- Understanding Counterexamples with explain -- Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement -- JNuke: Efficient Dynamic Analysis for Java -- The HiVy Tool Set -- ObsSlice: A Timed Automata Slicer Based on Observers -- The UCLID Decision Procedure -- MCK: Model Checking the Logic of Knowledge -- Zing: A Model Checker for Concurrent Software -- The Mec 5 Model-Checker -- PlayGame: A Platform for Diagnostic Games -- SAL 2 -- Formal Analysis of Java Programs in JavaFAN -- A Toolset for Modelling and Verification of GALS Systems -- WSAT: A Tool for Formal Analysis of Web Services -- CVC Lite: A New Implementation of the Cooperating Validity Checker -- CirCUs: A Satisfiability Solver Geared towards Bounded Model Checking -- Mechanical Mathematical Methods for Microprocessor Verification.Lecture Notes in Computer Science,0302-9743 ;3114ComputersSoftware engineeringLogic designComputer logicMathematical logicArtificial intelligenceTheory of Computationhttps://scigraph.springernature.com/ontologies/product-market-codes/I16005Software Engineeringhttps://scigraph.springernature.com/ontologies/product-market-codes/I14029Logic Designhttps://scigraph.springernature.com/ontologies/product-market-codes/I12050Logics and Meanings of Programshttps://scigraph.springernature.com/ontologies/product-market-codes/I1603XMathematical Logic and Formal Languageshttps://scigraph.springernature.com/ontologies/product-market-codes/I16048Artificial Intelligencehttps://scigraph.springernature.com/ontologies/product-market-codes/I21000Computers.Software engineering.Logic design.Computer logic.Mathematical logic.Artificial intelligence.Theory of Computation.Software Engineering.Logic Design.Logics and Meanings of Programs.Mathematical Logic and Formal Languages.Artificial Intelligence.005.1Alur Rajeevedthttp://id.loc.gov/vocabulary/relators/edtPeled Doron Aedthttp://id.loc.gov/vocabulary/relators/edtMiAaPQMiAaPQMiAaPQBOOK996465724703316Computer Aided Verification772228UNISA