Tools and Algorithms for the Construction and Analysis of Systems [[electronic resource] ] : 13th International Conference, TACAS 2007 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24 - April 1, 2007 Proceedings / / edited by Orna Grumberg, Michael Huth

• Record Nr.: UNISA996465474403316
• Pubbl/distr/stampa: Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007
• ISBN: 1-280-95188-5; 9786610951888; 3-540-71209-7
• Edizione: [1st ed. 2007.]
• Descrizione fisica: 1 online resource (755 p.)
• Collana: Theoretical Computer Science and General Issues, , 2512-2029 ; ; 4424
• Disciplina: 004.21
• Soggetti: Software engineering; Computer science; Computer networks; Algorithms; Software Engineering; Computer Science Logic and Foundations of Programming; Computer Communication Networks
• Lingua di pubblicazione: Inglese
• Formato: Materiale a stampa
• Livello bibliografico: Monografia
• Note generali: "... the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2007)"--Pref.
• Nota di bibliografia: Includes bibliographical references and index.
• Nota di contenuto: 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).