封面圖片

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

Saved in:
書目詳細資料
企業作者: SpringerLink (Online service)
其他作者: Namjoshi, Kedar. (Editor, http://id.loc.gov/vocabulary/relators/edt), Yoneda, Tomohiro. (Editor, http://id.loc.gov/vocabulary/relators/edt), Higashino, Teruo. (Editor, http://id.loc.gov/vocabulary/relators/edt), Okamura, Yoshio. (Editor, http://id.loc.gov/vocabulary/relators/edt)
格式: 電子 電子書
語言:English
出版: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2007.
版:1st ed. 2007.
叢編:Programming and Software Engineering ; 4762
主題:
Computer-aided engineering.
Computer logic.
Computers.
Computer communication systems.
Special purpose computers.
Software engineering.
Computer-Aided Engineering (CAD, CAE) and Design.
Logics and Meanings of Programs.
Information Systems and Communication Service.
Computer Communication Networks.
Special Purpose and Application-Based Systems.
Software Engineering.
在線閱讀:https://doi.org/10.1007/978-3-540-75596-8
標簽: 添加標簽
沒有標簽, 成為第一個標記此記錄!
書本目錄:
  • 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.

相似書籍