Umfang:
Online-Ressource (XX, 738 p. Also available online, digital)
ISBN:
9783540712091
Serie:
Lecture Notes in Computer Science 4424
Inhalt:
Invited Contributions -- THERE AND BACK AGAIN: Lessons Learned on the Way to the Market -- Verifying Object-Oriented Software: Lessons and Challenges -- Software Verification -- Shape Analysis by Graph Decomposition -- A Reachability Predicate for Analyzing Low-Level Software -- Generating Representation Invariants of Structurally Complex Data -- Probabilistic Model Checking and Markov Chains -- Multi-objective Model Checking of Markov Decision Processes -- PReMo: An Analyzer for Probabilistic Recursive Models -- Counterexamples in Probabilistic Model Checking -- Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking -- Static Analysis -- Causal Dataflow Analysis for Concurrent Programs -- Type-Dependence Analysis and Program Transformation for Symbolic Execution -- JPF–SE: A Symbolic Execution Extension to Java PathFinder -- Markov Chains and Real-Time Systems -- A Symbolic Algorithm for Optimal Markov Chain Lumping -- Flow Faster: Efficient Decision Algorithms for Probabilistic Simulations -- Model Checking Probabilistic Timed Automata with One or Two Clocks -- Adaptor Synthesis for Real-Time Components -- Timed Automata and Duration Calculus -- Deciding an Interval Logic with Accumulated Durations -- From Time Petri Nets to Timed Automata: An Untimed Approach -- Complexity in Simplicity: Flexible Agent-Based State Space Exploration -- On Sampling Abstraction of Continuous Time Logic with Durations -- Assume-Guarantee Reasoning -- Assume-Guarantee Synthesis -- Optimized L*-Based Assume-Guarantee Reasoning -- Refining Interface Alphabets for Compositional Verification -- MAVEN: Modular Aspect Verification -- Biological Systems -- Model Checking Liveness Properties of Genetic Regulatory Networks -- Checking Pedigree Consistency with PCS -- “Don’t Care” Modeling: A Logical Framework for Developing Predictive System Models -- Abstraction Refinement -- Deciding Bit-Vector Arithmetic with Abstraction -- Abstraction Refinement of Linear Programs with Arrays -- Property-Driven Partitioning for Abstraction Refinement -- Combining Abstraction Refinement and SAT-Based Model Checking -- Message Sequence Charts -- Detecting Races in Ensembles of Message Sequence Charts -- Replaying Play In and Play Out: Synthesis of Design Models from Scenarios by Learning -- Automata-Based Model Checking -- Improved Algorithms for the Automata-Based Approach to Model-Checking -- GOAL: A Graphical Tool for Manipulating Büchi Automata and Temporal Formulae -- Faster Algorithms for Finitary Games -- Specification Languages -- Planned and Traversable Play-Out: A Flexible Method for Executing Scenario-Based Programs, -- motor:The modest Tool Environment -- Syntactic Optimizations for PSL Verification -- The Heterogeneous Tool Set, Hets -- Security -- Searching for Shapes in Cryptographic Protocols -- Automatic Analysis of the Security of XOR-Based Key Management Schemes -- Software and Hardware Verification -- State of the Union: Type Inference Via Craig Interpolation -- Hoare Logic for Realistically Modelled Machine Code -- VCEGAR: Verilog CounterExample Guided Abstraction Refinement -- Decision Procedures and Theorem Provers -- Alloy Analyzer+PVS in the Analysis and Verification of Alloy Specifications -- Combined Satisfiability Modulo Parametric Theories -- A Gröbner Basis Approach to CNF-Formulae Preprocessing -- Kodkod: A Relational Model Finder -- Model Checking -- Bounded Reachability Checking of Asynchronous Systems Using Decision Diagrams -- Model Checking on Trees with Path Equivalences -- Uppaal/DMC – Abstraction-Based Heuristics for Directed Model Checking -- Distributed Analysis with ?CRL: A Compendium of Case Studies -- Infinite-State Systems -- A Generic Framework for Reasoning About Dynamic Networks of Infinite-State Processes -- Unfolding Concurrent Well-Structured Transition Systems -- Regular Model Checking Without Transducers (On Efficient Verification of Parameterized Systems).
Anmerkung:
Description based upon print version of record
,
""Title""; ""Foreword""; ""Preface""; ""Organization""; ""Table of Contents""; ""THERE AND BACK AGAIN: Lessons Learned on the Way to the Market""; ""Verifying Object-Oriented Software: Lessons and Challenges""; ""Shape Analysis by Graph Decomposition""; ""Introduction""; ""Overview""; ""A Full Heap Abstraction for Lists""; ""Abstracting List Segments""; ""A Graph Decomposition Abstraction for Lists""; ""The Abstract Domain of Shape Subgraphs""; ""Abstraction by Graph Decomposition""; ""Concretization by Composition of Shape Subgraphs""
,
""Developing Efficient Abstract Transformersfor the Graph Decomposition Abstraction""""The Most Precise Abstract Transformer""; ""Sound and Efficient Transformers""; ""An Incremental Transformer""; ""Prototype Implementation and Empirical Results""; ""Related Work""; ""A Reachability Predicate for Analyzing Low-Level Software""; ""Introduction""; ""Related Work""; ""Motivation""; ""Example""; ""Operational Semantics of C""; ""Reachability and Pointer Arithmetic""; ""Annotation Language""; ""Implementation""; ""Proving Verification Conditions""; ""Evaluation""; ""Conclusions and Future Work""
,
""Generating Representation Invariants of Structurally Complex Data""""Introduction""; ""Example""; ""Deryaft""; ""Program Heap as an Edge-Labeled Graph""; ""Core and Derived Fields""; ""Properties of Interest""; ""Algorithm""; ""Illustration: Binary Tree Representation of Heaps""; ""Experiments""; ""Discussion""; ""Related Work""; ""Conclusions""; ""Multi-objective Model Checking of Markov Decision Processes""; ""Introduction""; ""Basics and Background""; ""Multi-objective Reachability""; ""Qualitative Multi-objective Model Checking""; ""Quantitative Multi-objective Model Checking""
,
""Concluding Remarks""""PReMo: An Analyzer for Probabilistic Recursive Models""; ""Introduction""; ""Experimental Results""; ""Future Work""; ""Counterexamples in Probabilistic Model Checking""; ""Introduction""; ""Preliminaries""; ""Strongest Evidences and Counterexamples""; ""From a DTMC to a Weighted Digraph""; ""Finding Strongest Evidences""; ""Finding Smallest Counterexamples""; ""Lower Bounds on Probabilities""; ""Conclusion""; ""Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking""; ""Introduction""; ""Preliminaries""; ""Bisimulation""; ""Experiments""
,
""Discrete Time""""Continuous Time""; ""Rewards""; ""Concluding Remarks""; ""Causal Dataflow Analysis for Concurrent Programs""; ""Introduction""; ""Preliminaries""; ""The Control Net of a Program""; ""Causal Concurrent Dataflow Framework""; ""Meet over All Traces Solution""; ""Formulation of Specific Problems in the CCD Framework""; ""Solving the Distributive CCD Problem""; ""Experiments""; ""Conclusions""; ""Type-Dependence Analysis and Program Transformation for Symbolic Execution""; ""Introduction""; ""Type-Dependence Analysis""; ""Building the TDG""
,
""Performing CFL-Reachability on the TDG""
Weitere Ausg.:
ISBN 9783540712084
Weitere Ausg.:
Buchausg. u.d.T. Tools and algorithms for the construction and analysis of systems Berlin : Springer, 2007 ISBN 3540712089
Weitere Ausg.:
ISBN 9783540712084
Sprache:
Englisch
Fachgebiete:
Informatik
Schlagwort(e):
Systementwicklung
;
Softwareentwicklung
;
Model Checking
;
Programmanalyse
;
Theoretische Informatik
;
Systementwicklung
;
Softwareentwicklung
;
Model Checking
;
Programmanalyse
;
Theoretische Informatik
;
Konferenzschrift
DOI:
10.1007/978-3-540-71209-1
URL:
Volltext
(lizenzpflichtig)
URL:
Volltext
(lizenzpflichtig)
Bookmarklink
