Tools and Algorithms for the Construction and Analysis of Systems
Editat de Nicolas Halbwachs, Lenore Zucken Limba Engleză Paperback – 23 mar 2005
Preț: 637.87 lei
Preț vechi: 797.35 lei
-20% Nou
Puncte Express: 957
Preț estimativ în valută:
112.85€ • 131.68$ • 98.67£
112.85€ • 131.68$ • 98.67£
Carte tipărită la comandă
Livrare economică 17-31 ianuarie 26
Preluare comenzi: 021 569.72.76
Specificații
ISBN-13: 9783540253334
ISBN-10: 3540253335
Pagini: 612
Ilustrații: XVIII, 590 p.
Dimensiuni: 155 x 235 x 33 mm
Greutate: 0.91 kg
Ediția:2005
Editura: Springer
Locul publicării:Berlin, Heidelberg, Germany
ISBN-10: 3540253335
Pagini: 612
Ilustrații: XVIII, 590 p.
Dimensiuni: 155 x 235 x 33 mm
Greutate: 0.91 kg
Ediția:2005
Editura: Springer
Locul publicării:Berlin, Heidelberg, Germany
Public țintă
ResearchCuprins
Invited Paper.- Applications of Craig Interpolants in Model Checking.- Regular Model-Checking.- Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking.- Simulation-Based Iteration of Tree Transducers.- Using Language Inference to Verify Omega-Regular Properties.- Infinite State Systems.- On-the-Fly Reachability and Cycle Detection for Recursive State Machines.- Empirically Efficient Verification for a Class of Infinite-State Systems.- Context-Bounded Model Checking of Concurrent Software.- A Generic Theorem Prover of CSP Refinement.- Abstract Interpretation.- Separating Fairness and Well-Foundedness for the Analysis of Fair Discrete Systems.- An Abstract Interpretation-Based Refinement Algorithm for Strong Preservation.- Dependent Types for Program Understanding.- Automata and Logics.- A Note on On-the-Fly Verification Algorithms.- Truly On-the-Fly LTL Model Checking.- Complementation Constructions for Nondeterministic Automata on Infinite Words.- Using BDDs to Decide CTL.- Probabilistic Systems, Probabilistic Model-Checking.- Model Checking Infinite-State Markov Chains.- Algorithmic Verification of Recursive Probabilistic State Machines.- Monte Carlo Model Checking.- Satisfiability.- Efficient Conflict Analysis for Finding All Satisfying Assignments of a Boolean Circuit.- Bounded Validity Checking of Interval Duration Logic.- An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic.- A Two-Tier Technique for Supporting Quantifiers in a Lazily Proof-Explicating Theorem Prover.- Testing.- Symbolic Test Selection Based on Approximate Analysis.- Symstra: A Framework for Generating Object-Oriented Unit Tests Using Symbolic Execution.- Abstraction and Reduction.- Dynamic Symmetry Reduction.- Localization and Register Sharing for Predicate Abstraction.- On Some Transformation Invariants Under Retiming and Resynthesis.- Specification, Program Synthesis.- Compositional Message Sequence Charts (CMSCs) Are Better to Implement Than MSCs.- Temporal Logic for Scenario-Based Specifications.- Mining Temporal Specifications for Error Detection.- A New Algorithm for Strategy Synthesis in LTL Games.- Model-Checking.- Shortest Counterexamples for Symbolic Model Checking of LTL with Past.- Snapshot Verification.- Time-Efficient Model Checking with Magnetic Disk.- Tool Presentations.- jMoped: A Java Bytecode Checker Based on Moped.- Java-MOP: A Monitoring Oriented Programming Environment for Java.- JML-Testing-Tools: A Symbolic Animator for JML Specifications Using CLP.- jETI: A Tool for Remote Tool Integration.- FocusCheck: A Tool for Model Checking and Debugging Sequential C Programs.- SATABS: SAT-Based Predicate Abstraction for ANSI-C.- DiVer: SAT-Based Model Checking Platform for Verifying Large Scale Systems.- BISIMULATOR: A Modular Tool for On-the-Fly Equivalence Checking.