Automated Technology for Verification and Analysis
Springer Berlin (Verlag)
978-3-540-75595-1 (ISBN)
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.
| Erscheint lt. Verlag | 9.10.2007 |
|---|---|
| Reihe/Serie | Lecture Notes in Computer Science | Programming and Software Engineering |
| Zusatzinfo | XIV, 570 p. |
| Verlagsort | Berlin |
| Sprache | englisch |
| Maße | 155 x 235 mm |
| Gewicht | 872 g |
| Themenwelt | Informatik ► Weitere Themen ► CAD-Programme |
| Schlagworte | Automata • Construction • Embedded Systems • Formal Method • formal methods • formal performance analysis • Hardcover, Softcover / Informatik, EDV/Informatik • hardware verification • HC/Informatik, EDV/Informatik • Hybrid Systems • Model Checking • Modeling • Petri net • Petri Nets • Probabilistic Models • program analysis • Protocol Verification • real-time • Real-Time Systems • Refinement • Simulation • Software Verification • Systems Analysis • Systems Design • systems verification • timed systems • Validation • verification |
| ISBN-10 | 3-540-75595-0 / 3540755950 |
| ISBN-13 | 978-3-540-75595-1 / 9783540755951 |
| Zustand | Neuware |
| Haben Sie eine Frage zum Produkt? |
aus dem Bereich
