Cover Image
Read Now

Automated Technology for Verification and Analysis 5th International Symposium, ATVA 2007 Tokyo, Japan, October 22-25, 2007 Proceedings

Bibliographic Details
Other Authors: Namjoshi, Kedar (Editor), Yoneda, Tomohiro (Editor), Higashino, Teruo (Editor), Okamura, Yoshio (Editor)
Format: eBook
Language:English
Published: Berlin, Heidelberg Springer Berlin Heidelberg 2007, 2007
Edition:1st ed. 2007
Series:Programming and Software Engineering
Subjects:
Computer Communication Networks
Computer Science Logic And Foundations Of Programming
Software Engineering
Computer Science
Computer-aided Engineering (cad, Cae) And Design
Computer Networks 
Computer-aided Engineering
Special Purpose And Application-based Systems
Computers, Special Purpose
Online Access:
Collection: Springer eBooks 2005- - Collection details see MPG.ReNa
Table of Contents:
  • 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

Similar Items