Tools and Algorithms for the Construction and Analysis of Systems

ETAPS 2010 was the 13th instance of the European Joint Conferences on T- oryandPracticeofSoftware. ETAPSisanannualfederatedconferencethatwas establishedin1998bycombininganumberofexistingandnewconferences. This yearitcomprisedtheusual?vesisterconferences(CC,ESOP,FASE,FOSSACS, TACAS), 19 satellite workshops (ACCAT, ARSPA-WITS, Bytecode, CMCS, COCV, DCC, DICE, FBTC, FESCA, FOSS-AMA, GaLoP, GT-VMT, LDTA, MBT, PLACES, QAPL, SafeCert, WGT, and WRLA) and seven invited l- tures (excluding those that were speci?c to the satellite events). The ?ve main conferences this year received 497 submissions (including 31 tool demonstration papers), 130 of which were accepted (10 tool demos), giving an overall acc- tance rateof 26%, with most of the conferencesat around24%. Congratulations thereforetoalltheauthorswhomadeittothe?nalprogramme!Ihopethatmost of the other authors will still have found a way of participating in this exciting event, and that you will all continue submitting to ETAPS and contributing to make of it the best conference on software science and engineering. The events that comprise ETAPS address various aspects of the system - velopmentprocess,including speci?cation,design, implementation, analysisand improvement. The languages, methodologies and tools which support these - tivities are all well within its scope. Di?erent blends of theory and practice are represented,withaninclinationtowardtheorywithapracticalmotivationonthe one hand and soundly based practice on the other. Many of the issues involved in software design apply to systems in general, including hardwaresystems, and the emphasis on software is not intended to be exclusive. ETAPS is a confederation in which each event retains its own identity, with a separate Programme Committee and proceedings. Its format is open-ended, allowing it to grow and evolve as time goes by.

Fast track conference proceedings State of the art papers Up to date research

Klappentext

This book constitutes the refereed proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010, held in Paphos, Cyprus, in March 2010, as part of ETAPS 2010, the European Joint Conferences on Theory and Practice of Software. The 35 papers presented were carefully reviewed and selected from 134 submissions. The topics covered are probabilistic systems and optimization, decision procedures, tools, automata theory, liveness, software verification, real time and information flow, and testing.

Inhalt
Invited Talks.- Embedded Systems Design Scientific Challenges and Work Directions.- Antichain Algorithms for Finite Automata.- Probabilistic Systems and Optimization.- Assume-Guarantee Verification for Probabilistic Systems.- Simple O(m logn) Time Markov Chain Lumping.- Model Checking Interactive Markov Chains.- Approximating the Pareto Front of Multi-criteria Optimization Problems.- Decision Procedures.- An Alternative to SAT-Based Approaches for Bit-Vectors.- Satisfiability Modulo the Theory of Costs: Foundations and Applications.- Optimal Tableau Algorithms for Coalgebraic Logics.- Blocked Clause Elimination.- Tools I.- Boom: Taking Boolean Program Model Checking One Step Further.- The OpenSMT Solver.- Stranger: An Automata-Based String Analysis Tool for PHP.- Automata Theory.- When Simulation Meets Antichains.- On Weak Modal Compatibility, Refinement, and the MIO Workbench.- Rational Synthesis.- Efficient Büchi Universality Checking.- Liveness.- Automated Termination Analysis for Programs with Second-Order Recursion.- Ranking Function Synthesis for Bit-Vector Relations.- Fairness for Dynamic Control.- Tools II.- JTorX: A Tool for On-Line Model-Driven Test Derivation and Execution.- SLAB: A Certifying Model Checker for Infinite-State Concurrent Systems.- Tracking Heaps That Hop with Heap-Hop.- Software Verification.- Automatic Analysis of Scratch-Pad Memory Code for Heterogeneous Multicore Processors.- Simplifying Linearizability Proofs with Reduction and Abstraction.- A Polymorphic Intermediate Verification Language: Design and Logical Encoding.- Trace-Based Symbolic Analysis for Atomicity Violations.- Tools III.- ACS: Automatic Converter Synthesis for SoC Bus Protocols.- AlPiNA: An Algebraic Petri Net Analyzer.- PASS: Abstraction Refinement for InfiniteProbabilistic Models.- Real Time and Information Flow.- Arrival Curves for Real-Time Calculus: The Causality Problem and Its Solutions.- Computing the Leakage of Information-Hiding Systems.- Statistical Measurement of Information Leakage.- SAT Based Bounded Model Checking with Partial Order Semantics for Timed Automata.- Testing.- Preemption Sealing for Efficient Concurrency Testing.- Code Mutation in Verification and Automatic Code Correction.- Efficient Detection of Errors in Java Components Using Random Environment and Restarts.