Automated Technology for Verification and Analysis  5th International Symposium, ATVA 2007 Tokyo, Japan, October 22-25, 2007 Proceedings /  [electronic resource] : 
edited by Kedar Namjoshi, Tomohiro Yoneda, Teruo Higashino, Yoshio Okamura. 
 - 1st ed. 2007. 
 - XIV, 570 p.  online resource. 
 - Programming and Software Engineering,  4762  2945-9168 ; .
 - Programming and Software Engineering,  4762 .
<br/><br/>Invited 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. 
<br/><br/><label>ISBN: </label>9783540755968 
<br/><br/><label>Standard No.: </label>10.1007/978-3-540-75596-8  doi 
<br/><br/><label>Subjects--Topical Terms: </label><br/>Computer-aided engineering.<br/>Computer science.<br/>Computer networks .<br/>Computers, Special purpose.<br/>Software engineering.<br/>Computer-Aided Engineering (CAD, CAE) and Design.<br/>Computer Science Logic and Foundations of Programming.<br/>Computer Communication Networks.<br/>Special Purpose and Application-Based Systems.<br/>Software Engineering.
<br/><br/><label>LC Class. No.: </label>TA345-345.5 
<br/><br/><label>Dewey Class. No.: </label>670.285