Tools and Algorithms for the Construction and Analysis of Systems

Table of Contents

1. Altmetric Badge
   Book Overview
2. Altmetric Badge
   Chapter 1 Scalable Timing Analysis with Refinement
3. Altmetric Badge
   Chapter 2 A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System
4. Altmetric Badge
   Chapter 3 Verified Reachability Analysis of Continuous Systems
5. Altmetric Badge
   Chapter 4 HyComp : An SMT-Based Model Checker for Hybrid Systems
6. Altmetric Badge
   Chapter 5 C2E2: A Verification Tool for Stateflow Models
7. Altmetric Badge
   Chapter 6 Non-cumulative Resource Analysis
8. Altmetric Badge
   Chapter 7 Value Slice: A New Slicing Concept for Scalable Property Checking
9. Altmetric Badge
   Chapter 8 A Method for Improving the Precision and Coverage of Atomicity Violation Predictions
10. Altmetric Badge
    Chapter 9 Commutativity of Reducers
11. Altmetric Badge
    Chapter 10 Inferring Simple Solutions to Recursion-Free Horn Clauses via Sampling
12. Altmetric Badge
    Chapter 11 Analysis of Dynamic Process Networks
13. Altmetric Badge
    Chapter 12 MultiGain : A Controller Synthesis Tool for MDPs with Multiple Mean-Payoff Objectives
14. Altmetric Badge
    Chapter 13 syntMaskFT: A Tool for Synthesizing Masking Fault-Tolerant Programs from Deontic Specifications
15. Altmetric Badge
    Chapter 14 νZ - An Optimizing SMT Solver
16. Altmetric Badge
    Chapter 15 dReach : δ -Reachability Analysis for Hybrid Systems
17. Altmetric Badge
    Chapter 16 Uppaal Stratego
18. Altmetric Badge
    Chapter 17 BINSEC: Binary Code Analysis with Low-Level Regions
19. Altmetric Badge
    Chapter 18 Insight: An Open Binary Analysis Framework
20. Altmetric Badge
    Chapter 19 SAM: The Static Analysis Module of the MAVERIC Mobile App Security Verification Platform
21. Altmetric Badge
    Chapter 20 Symbolic Model-Checking Using ITS-Tools
22. Altmetric Badge
    Chapter 21 Semantic Importance Sampling for Statistical Model Checking
23. Altmetric Badge
    Chapter 22 Strategy Synthesis for Stochastic Games with Multiple Long-Run Objectives
24. Altmetric Badge
    Chapter 23 FAUST $^{\mathsf 2}$ : Formal Abstractions of Uncountable-STate STochastic Processes
25. Altmetric Badge
    Chapter 24 Linearly Ordered Attribute Grammar Scheduling Using SAT-Solving
26. Altmetric Badge
    Chapter 25 On Parallel Scalable Uniform SAT Witness Generation
27. Altmetric Badge
    Chapter 26 Approximate Counting in SMT and Value Estimation for Probabilistic Programs
28. Altmetric Badge
    Chapter 27 Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions
29. Altmetric Badge
    Chapter 28 Stateless Model Checking for TSO and PSO
30. Altmetric Badge
    Chapter 29 GPU Accelerated Strong and Branching Bisimilarity Checking
31. Altmetric Badge
    Chapter 30 Fairness for Infinite-State Systems
32. Altmetric Badge
    Chapter 31 Software Verification and Verifiable Witnesses
33. Altmetric Badge
    Chapter 32 AProVE : Termination and Memory Safety of C Programs
34. Altmetric Badge
    Chapter 33 Cascade
35. Altmetric Badge
    Chapter 34 CPAchecker with Support for Recursive Programs and Floating-Point Arithmetic
36. Altmetric Badge
    Chapter 35 CPArec : Verifying Recursive Programs via Source-to-Source Program Transformation
37. Altmetric Badge
    Chapter 36 FramewORk for Embedded System verification
38. Altmetric Badge
    Chapter 37 Forester: Shape Analysis Using Tree Automata
39. Altmetric Badge
    Chapter 38 MU-CSeq 0.3: Sequentialization by Read-Implicit and Coarse-Grained Memory Unwindings
40. Altmetric Badge
    Chapter 39 Perentie: Modular Trace Refinement and Selective Value Tracking
41. Altmetric Badge
    Chapter 40 Predator Hunting Party (Competition Contribution)
42. Altmetric Badge
    Chapter 41 SeaHorn: A Framework for Verifying C Programs (Competition Contribution)
43. Altmetric Badge
    Chapter 42 SMACK+Corral: A Modular Verifier
44. Altmetric Badge
    Chapter 43 Ultimate Automizer with Array Interpolation
45. Altmetric Badge
    Chapter 44 ULTIMATE KOJAK with Memory Safety Checks
46. Altmetric Badge
    Chapter 45 Unbounded Lazy-CSeq: A Lazy Sequentialization Tool for C Programs with Unbounded Context Switches
47. Altmetric Badge
    Chapter 46 FuncTion: An Abstract Domain Functor for Termination
48. Altmetric Badge
    Chapter 47 Model Checking Gene Regulatory Networks
49. Altmetric Badge
    Chapter 48 Symbolic Quantitative Robustness Analysis of Timed Automata
50. Altmetric Badge
    Chapter 49 Pattern-Based Refinement of Assume-Guarantee Specifications in Reactive Synthesis
51. Altmetric Badge
    Chapter 50 Assume-Guarantee Synthesis for Concurrent Reactive Programs with Partial Information
52. Altmetric Badge
    Chapter 51 Shield Synthesis:
53. Altmetric Badge
    Chapter 52 Verifying Concurrent Programs by Memory Unwinding
54. Altmetric Badge
    Chapter 53 AutoProof: Auto-Active Functional Verification of Object-Oriented Programs
55. Altmetric Badge
    Chapter 54 An LTL Proof System for Runtime Verification
56. Altmetric Badge
    Chapter 55 MarQ: Monitoring at Runtime with QEA
57. Altmetric Badge
    Chapter 56 Parallel Explicit Model Checking for Generalized Büchi Automata
58. Altmetric Badge
    Chapter 57 Limit Deterministic and Probabilistic Automata for LTL ∖ GU
59. Altmetric Badge
    Chapter 58 Saturation-Based Incremental LTL Model Checking with Inductive Proofs
60. Altmetric Badge
    Chapter 59 Nested Antichains for WS1S
61. Altmetric Badge
    Chapter 60 Sylvan: Multi-Core Decision Diagrams
62. Altmetric Badge
    Chapter 61 LTSmin: High-Performance Language-Independent Model Checking
63. Altmetric Badge
    Chapter 62 Using a Formal Model to Improve Verification of a Cache-Coherent System-on-Chip