LEADER 07094nam 22008775 450 001 996465920803316 005 20200703042935.0 010 $a3-540-75596-9 024 7 $a10.1007/978-3-540-75596-8 035 $a(CKB)1000000000490357 035 $a(SSID)ssj0000316404 035 $a(PQKBManifestationID)11285846 035 $a(PQKBTitleCode)TC0000316404 035 $a(PQKBWorkID)10275883 035 $a(PQKB)11488387 035 $a(DE-He213)978-3-540-75596-8 035 $a(MiAaPQ)EBC6284238 035 $a(MiAaPQ)EBC337375 035 $a(MiAaPQ)EBC4976479 035 $a(Au-PeEL)EBL337375 035 $a(OCoLC)808680858 035 $a(PPN)123728649 035 $a(EXLCZ)991000000000490357 100 $a20100301d2007 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aAutomated Technology for Verification and Analysis$b[electronic resource] $e5th International Symposium, ATVA 2007 Tokyo, Japan, October 22-25, 2007 Proceedings /$fedited by Kedar Namjoshi, Tomohiro Yoneda, Teruo Higashino, Yoshio Okamura 205 $a1st ed. 2007. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2007. 215 $a1 online resource (XIV, 570 p.) 225 1 $aProgramming and Software Engineering ;$v4762 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-540-75595-0 320 $aIncludes bibliographical references and index. 327 $aInvited Talks -- Policies and Proofs for Code Auditing -- Recent Trend in Industry and Expectation to DA Research -- Toward Property-Driven Abstraction for Heap Manipulating Programs -- Branching vs. Linear Time: Semantical Perspective -- Regular Papers -- Mind the Shapes: Abstraction Refinement Via Topology Invariants -- Complete SAT-Based Model Checking for Context-Free Processes -- Bounded Model Checking of Analog and Mixed-Signal Circuits Using an SMT Solver -- Model Checking Contracts ? A Case Study -- On the Efficient Computation of the Minimal Coverability Set for Petri Nets -- Analog/Mixed-Signal Circuit Verification Using Models Generated from Simulation Traces -- Automatic Merge-Point Detection for Sequential Equivalence Checking of System-Level and RTL Descriptions -- Proving Termination of Tree Manipulating Programs -- Symbolic Fault Tree Analysis for Reactive Systems -- Computing Game Values for Crash Games -- Timed Control with Observation Based and Stuttering Invariant Strategies -- Deciding Simulations on Probabilistic Automata -- Mechanizing the Powerset Construction for Restricted Classes of ?-Automata -- Verifying Heap-Manipulating Programs in an SMT Framework -- A Generic Constructive Solution for Concurrent Games with Expressive Constraints on Strategies -- Distributed Synthesis for Alternating-Time Logics -- Timeout and Calendar Based Finite State Modeling and Verification of Real-Time Systems -- Efficient Approximate Verification of Promela Models Via Symmetry Markers -- Latticed Simulation Relations and Games -- Providing Evidence of Likely Being on Time: Counterexample Generation for CTMC Model Checking -- Assertion-Based Proof Checking of Chang-Roberts Leader Election in PVS -- Continuous Petri Nets: Expressive Power and Decidability Issues -- Quantifying the Discord: Order Discrepancies in Message Sequence Charts -- A Formal Methodology to Test Complex Heterogeneous Systems -- A New Approach to Bounded Model Checking for Branching Time Logics -- Exact State Set Representations in the Verification of Linear Hybrid Systems with Large Discrete State Space -- A Compositional Semantics for Dynamic Fault Trees in Terms of Interactive Markov Chains -- 3-Valued Circuit SAT for STE with Automatic Refinement -- Bounded Synthesis -- Short Papers -- Formal Modeling and Verification of High-Availability Protocol for Network Security Appliances -- A Brief Introduction to -- On-the-Fly Model Checking of Fair Non-repudiation Protocols -- Model Checking Bounded Prioritized Time Petri Nets -- Using Patterns and Composite Propositions to Automate the Generation of LTL Specifications -- Pruning State Spaces with Extended Beam Search -- Using Counterexample Analysis to Minimize the Number of Predicates for Predicate Abstraction. 330 $aThis book constitutes the refereed proceedings of the 5th International Symposium on Automated Technology for Verification and Analysis, ATVA 2007, held in Tokyo, Japan, October 22-25, 2007. The 29 revised full papers presented together with 7 short papers were carefully reviewed and selected from 88 submissions. The papers address theoretical methods to achieve correct software or hardware systems, including both functional and non functional aspects; as well as applications of theory in engineering methods and particular domains and handling of practical problems occurring in tools. 410 0$aProgramming and Software Engineering ;$v4762 606 $aComputer-aided engineering 606 $aComputer logic 606 $aComputers 606 $aComputer communication systems 606 $aSpecial purpose computers 606 $aSoftware engineering 606 $aComputer-Aided Engineering (CAD, CAE) and Design$3https://scigraph.springernature.com/ontologies/product-market-codes/I23044 606 $aLogics and Meanings of Programs$3https://scigraph.springernature.com/ontologies/product-market-codes/I1603X 606 $aInformation Systems and Communication Service$3https://scigraph.springernature.com/ontologies/product-market-codes/I18008 606 $aComputer Communication Networks$3https://scigraph.springernature.com/ontologies/product-market-codes/I13022 606 $aSpecial Purpose and Application-Based Systems$3https://scigraph.springernature.com/ontologies/product-market-codes/I13030 606 $aSoftware Engineering$3https://scigraph.springernature.com/ontologies/product-market-codes/I14029 615 0$aComputer-aided engineering. 615 0$aComputer logic. 615 0$aComputers. 615 0$aComputer communication systems. 615 0$aSpecial purpose computers. 615 0$aSoftware engineering. 615 14$aComputer-Aided Engineering (CAD, CAE) and Design. 615 24$aLogics and Meanings of Programs. 615 24$aInformation Systems and Communication Service. 615 24$aComputer Communication Networks. 615 24$aSpecial Purpose and Application-Based Systems. 615 24$aSoftware Engineering. 676 $a511.36028563 702 $aNamjoshi$b Kedar$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aYoneda$b Tomohiro$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aHigashino$b Teruo$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aOkamura$b Yoshio$4edt$4http://id.loc.gov/vocabulary/relators/edt 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a996465920803316 996 $aAutomated Technology for Verification and Analysis$9772478 997 $aUNISA