Tools and Algorithms for the Construction and Analysis of Systems

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.