Tools and Algorithms for the Construction and Analysis of Systems: 15th International Conference, Tacas 2009, Held as Part of the Joint European Confe

ISBN-13: 9783642007675 / Angielski / Miękka / 2009 / 456 str.

Stefan Kowalewski

Opis

ETAPS 2009 was the 12th instance of the European Joint Conferences on T- oryand Practiceof Software. ETAPS is anannual federatedconference that was establishedin1998bycombininganumberofexistingandnewconferences. This year it comprised ?ve conferences (CC, ESOP, FASE, FOSSACS, TACAS), 22 satellite workshops (ACCAT, ARSPA-WITS, Bytecode, COCV, COMPASS, FESCA, FInCo, FORMED, GaLoP, GT-VMT, HFL, LDTA, MBT, MLQA, OpenCert, PLACES, QAPL, RC, SafeCert, TAASN, TERMGRAPH, and WING), fourtutorials, andseveninvitedlectures(excludingthosethatweres- ci?c to the satellite events). The ?ve main conferences received 532 submissions (including 30 tool demonstration papers), 141 of which were accepted (10 tool demos), giving an overall acceptance rate of about 26%, with most of the c- ferences at around 25%. Congratulations therefore to all the authors who made it to the ?nal programme I hope that most of the other authors will still have found a way of participating in this exciting event, and that youwill allcontinue submitting to ETAPS and contributing towards making it the best conference on software science and engineering. The events that comprise ETAPS address various aspects of the system - velopment process, including speci?cation, design, implementation, analysis and 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, with an inclination towards theory with a practical motivation on the one hand and soundly based practice on the other. Many of the issues involved in software design apply to systems in general, including hardware s- tems, and the emphasis on software is not intended to be exclusive.

Spis treści

Model Checking I.- Hierarchical Set Decision Diagrams and Regular Models.- Büchi Complementation and Size-Change Termination.- Learning Minimal Separating DFA’s for Compositional Verification.- Tools I.- RBAC-PAT: A Policy Analysis Tool for Role Based Access Control.- ITPN-PerfBound: A Performance Bound Tool for Interval Time Petri Nets.- Romeo: A Parametric Model-Checker for Petri Nets with Stopwatches.- Alpaga: A Tool for Solving Parity Games with Imperfect Information.- Game-Theoretic Approaches.- Compositional Predicate Abstraction from Game Semantics.- Compositional Synthesis of Reactive Systems from Live Sequence Chart Specifications.- Computing Weakest Strategies for Safety Games of Imperfect Information.- Verification of Concurrent Programs.- Context-Bounded Analysis for Concurrent Programs with Dynamic Creation of Threads.- Semantic Reduction of Thread Interleavings in Concurrent Programs.- Inferring Synchronization under Limited Observability.- The Complexity of Predicting Atomicity Violations.- Tools II.- MoonWalker: Verification of .NET Programs.- Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays.- The Yogi Project: Software Property Checking via Static Analysis and Testing.- TaPAS: The Talence Presburger Arithmetic Suite.- Model Checking II.- Transition-Based Directed Model Checking.- Memoised Garbage Collection for Software Model Checking.- Hierarchical Adaptive State Space Caching Based on Level Sampling.- Parametric Analysis.- Static Analysis Techniques for Parameterised Boolean Equation Systems.- Parametric Trace Slicing and Monitoring.- Generative Approaches.- From Tests to Proofs.- Test Input Generation for Programs with Pointers.- Specification Mining with Few False Positives.- Program Analysis.- Path Feasibility Analysis for String-Manipulating Programs.- Symbolic String Verification: Combining String Analysis and Size Analysis.- Iterating Octagons.- Verifying Reference Counting Implementations.- Hybrid Systems.- Falsification of LTL Safety Properties in Hybrid Systems.- Computing Optimized Representations for Non-convex Polyhedra by Detection and Removal of Redundant Linear Constraints.- Decision Procedures and Theorem Proving.- All-Termination(T).- Ground Interpolation for the Theory of Equality.- Satisfiability Procedures for Combination of Theories Sharing Integer Offsets.- Invited Contribution.- Bridging the Gap Between Model-Based Development and Model Checking.

Blurb

This book constitutes the refereed proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2009, held in York, UK, in March 2009, as part of ETAPS 2009, the European Joint Conferences on Theory and Practice of Software.

The 27 full papers and 8 tool demonstrations included in the volume were thoroughly reviewed and selected from 131 submissions. The papers are organized in topical sections on Model Checking, Tools, Verification of Concurrent Programs, Parametric Analysis, Program Analysis, and Hybrid Systems.