Tools and Algorithms for the Construction and Analysis of Systems: 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings

Front Matter....Pages 1-18
Front Matter....Pages 1-1
Scalable Timing Analysis with Refinement....Pages 3-18
Front Matter....Pages 19-19
A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System....Pages 21-36
Verified Reachability Analysis of Continuous Systems....Pages 37-51
 HyComp : An SMT-Based Model Checker for Hybrid Systems....Pages 52-67
C2E2: A Verification Tool for Stateflow Models....Pages 68-82
Front Matter....Pages 83-83
Non-cumulative Resource Analysis....Pages 85-100
Value Slice: A New Slicing Concept for Scalable Property Checking....Pages 101-115
A Method for Improving the Precision and Coverage of Atomicity Violation Predictions....Pages 116-130
Commutativity of Reducers....Pages 131-146
Front Matter....Pages 147-147
Inferring Simple Solutions to Recursion-Free Horn Clauses via Sampling....Pages 149-163
Analysis of Dynamic Process Networks....Pages 164-178
Front Matter....Pages 179-179
 MultiGain : A Controller Synthesis Tool for MDPs with Multiple Mean-Payoff Objectives....Pages 181-187
syntMaskFT: A Tool for Synthesizing Masking Fault-Tolerant Programs from Deontic Specifications....Pages 188-193
 νZ - An Optimizing SMT Solver....Pages 194-199
 dReach : δ -Reachability Analysis for Hybrid Systems....Pages 200-205
 Uppaal Stratego ....Pages 206-211
BINSEC: Binary Code Analysis with Low-Level Regions....Pages 212-217
Insight: An Open Binary Analysis Framework....Pages 218-224
SAM: The Static Analysis Module of the MAVERIC Mobile App Security Verification Platform....Pages 225-230
Symbolic Model-Checking Using ITS-Tools....Pages 231-237
Front Matter....Pages 239-239
Semantic Importance Sampling for Statistical Model Checking....Pages 241-255
Strategy Synthesis for Stochastic Games with Multiple Long-Run Objectives....Pages 256-271
 FAUST $^{\mathsf 2}$ : F ormal A bstractions of U ncountable- ST ate ST ochastic Processes....Pages 272-286
Front Matter....Pages 287-287
Linearly Ordered Attribute Grammar Scheduling Using SAT-Solving....Pages 289-303
On Parallel Scalable Uniform SAT Witness Generation....Pages 304-319
Approximate Counting in SMT and Value Estimation for Probabilistic Programs....Pages 320-334
Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions....Pages 335-349
Front Matter....Pages 351-351
Stateless Model Checking for TSO and PSO....Pages 353-367
GPU Accelerated Strong and Branching Bisimilarity Checking....Pages 368-383
Fairness for Infinite-State Systems....Pages 384-398
Front Matter....Pages 399-399
Software Verification and Verifiable Witnesses....Pages 401-416
 AProVE : Termination and Memory Safety of C Programs....Pages 417-419
Cascade....Pages 420-422
 CPAchecker with Support for Recursive Programs and Floating-Point Arithmetic....Pages 423-425
 CPArec : Verifying Recursive Programs via Source-to-Source Program Transformation....Pages 426-428
FramewORk for Embedded System verification....Pages 429-431
Forester: Shape Analysis Using Tree Automata....Pages 432-435
MU-CSeq 0.3: Sequentialization by Read-Implicit and Coarse-Grained Memory Unwindings....Pages 436-438
Perentie: Modular Trace Refinement and Selective Value Tracking....Pages 439-442
Predator Hunting Party (Competition Contribution)....Pages 443-446
Front Matter....Pages 399-399
SeaHorn: A Framework for Verifying C Programs (Competition Contribution)....Pages 447-450
SMACK+Corral: A Modular Verifier....Pages 451-454
 Ultimate Automizer with Array Interpolation....Pages 455-457
ULTIMATE KOJAK with Memory Safety Checks....Pages 458-460
Unbounded Lazy-CSeq: A Lazy Sequentialization Tool for C Programs with Unbounded Context Switches....Pages 461-463
FuncTion: An Abstract Domain Functor for Termination....Pages 464-466
Front Matter....Pages 467-467
Model Checking Gene Regulatory Networks....Pages 469-483
Symbolic Quantitative Robustness Analysis of Timed Automata....Pages 484-498
Front Matter....Pages 499-499
Pattern-Based Refinement of Assume-Guarantee Specifications in Reactive Synthesis....Pages 501-516
Assume-Guarantee Synthesis for Concurrent Reactive Programs with Partial Information....Pages 517-532
Shield Synthesis:....Pages 533-548
Front Matter....Pages 549-549
Verifying Concurrent Programs by Memory Unwinding....Pages 551-565
AutoProof: Auto-Active Functional Verification of Object-Oriented Programs....Pages 566-580
An LTL Proof System for Runtime Verification....Pages 581-595
 MarQ : Monitoring at Runtime with QEA....Pages 596-610
Front Matter....Pages 611-611
Parallel Explicit Model Checking for Generalized Büchi Automata....Pages 613-627
Limit Deterministic and Probabilistic Automata for LTL ∖ GU....Pages 628-642
Saturation-Based Incremental LTL Model Checking with Inductive Proofs....Pages 643-657
Nested Antichains for WS1S....Pages 658-674
Front Matter....Pages 675-675
Sylvan: Multi-Core Decision Diagrams....Pages 677-691
Front Matter....Pages 675-675
LTSmin: High-Performance Language-Independent Model Checking....Pages 692-707
Using a Formal Model to Improve Verification of a Cache-Coherent System-on-Chip....Pages 708-722
Back Matter....Pages 723-725