000 05301nam a22006135i 4500
001 978-3-540-75596-8
003 DE-He213
005 20240423125313.0
007 cr nn 008mamaa
008 100301s2007 gw | s |||| 0|eng d
020 _a9783540755968
_9978-3-540-75596-8
024 7 _a10.1007/978-3-540-75596-8
_2doi
050 4 _aTA345-345.5
072 7 _aUGC
_2bicssc
072 7 _aCOM007000
_2bisacsh
072 7 _aUGC
_2thema
082 0 4 _a670.285
_223
245 1 0 _aAutomated Technology for Verification and Analysis
_h[electronic resource] :
_b5th International Symposium, ATVA 2007 Tokyo, Japan, October 22-25, 2007 Proceedings /
_cedited by Kedar Namjoshi, Tomohiro Yoneda, Teruo Higashino, Yoshio Okamura.
250 _a1st ed. 2007.
264 1 _aBerlin, Heidelberg :
_bSpringer Berlin Heidelberg :
_bImprint: Springer,
_c2007.
300 _aXIV, 570 p.
_bonline resource.
336 _atext
_btxt
_2rdacontent
337 _acomputer
_bc
_2rdamedia
338 _aonline resource
_bcr
_2rdacarrier
347 _atext file
_bPDF
_2rda
490 1 _aProgramming and Software Engineering,
_x2945-9168 ;
_v4762
505 0 _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.
650 0 _aComputer-aided engineering.
650 0 _aComputer science.
650 0 _aComputer networks .
650 0 _aComputers, Special purpose.
650 0 _aSoftware engineering.
650 1 4 _aComputer-Aided Engineering (CAD, CAE) and Design.
650 2 4 _aComputer Science Logic and Foundations of Programming.
650 2 4 _aComputer Communication Networks.
650 2 4 _aSpecial Purpose and Application-Based Systems.
650 2 4 _aSoftware Engineering.
700 1 _aNamjoshi, Kedar.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
700 1 _aYoneda, Tomohiro.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
700 1 _aHigashino, Teruo.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
700 1 _aOkamura, Yoshio.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
710 2 _aSpringerLink (Online service)
773 0 _tSpringer Nature eBook
776 0 8 _iPrinted edition:
_z9783540755951
776 0 8 _iPrinted edition:
_z9783540844938
830 0 _aProgramming and Software Engineering,
_x2945-9168 ;
_v4762
856 4 0 _uhttps://doi.org/10.1007/978-3-540-75596-8
912 _aZDB-2-SCS
912 _aZDB-2-SXCS
912 _aZDB-2-LNC
942 _cSPRINGER
999 _c176478
_d176478