Tools and Algorithms for the Construction and Analysis of Systems: 23rd International Conference, Tacas 2017, Held as Part of the European Joint Confe

ISBN-13: 9783662545799 / Angielski / Miękka / 2017 / 411 str.

Axel Legay; Tiziana Margaria

Spis treści

Security.- Static Detection of DoS Vulnerabilities in Programs that use Regular Expressions.- Discriminating Traces with Time.- Directed Automated Memory Performance Testing.- Context-bounded Analysis for POWER.- Run-Time Verification and Logic. -Rewriting-Based Runtime Verification of Alternation-Free HyperLTL Formulas.- Almost Event-Rate Independent Monitoring of Metric Temporal Logic.- Optimal Translation of LTL to Limit Deterministic Automata.- Quantitative Systems.- Sequential Convex Programming for the Efficient Verification of Parametric MDPs.- JANI: Quantitative Model and Tool Interaction.- Computing Scores of Forwarding Schemes in Switched Networks with Probabilistic Faults.- Long-run Rewards for Markov Automata.- SAT and SMT.- HiFrog: SMT-based Function Summarization for Software Verification.- Congruence Closure with Free Variables.- On Optimization Modulo Theories, MaxSMT and Sorting Networks. - The automatic detection of token structures and invariants using SAT checking.- Maximizing the Conditional Expected Reward for Reaching the Goal. -ARES: Adaptive Receding-Horizon Synthesis of Optimal Plans. - FlyFast: A Mean Field Model Checker. -ERODE: A Tool for the Evaluation and Reduction of Ordinary Differential Equations.- SV COMP.- Software Verification with Validation of Results (Report on SV-COMP 2017).- AProVE: Proving and Disproving Termination of Memory-Manipulating C Programs (Competition Contribution).- CPA-BAM-BnB: Block-Abstraction Memoization and Region-based Memory Models for Predicate Abstractions (Competition Contribution).- DepthK: A k-Induction Verifier Based on Invariant Inference for C Programs (Competition Contribution).- Forester: From Heap Shapes to Automata Predicates (Competition Contribution).- HipTNT+: A Termination and Non-termination Analyzer by Second-order Abduction (Competition Contribution).- Lazy-CSeq 2.0: Combining Lazy Sequentialization with Abstract Interpretation (Competition Contribution).- Skink: Static Analysis of LLVM Intermediate Representation (Competition contribution).- Symbiotic 4: Beyond Reachability (Competition Contribution).- Optimizing and Caching SMT Queries in SymDIVINE (Competition Contribution).- Ultimate Automizer with an On-demand Construction of Floyd-Hoare Automata (Competition Contribution).- Ultimate Taipan: Trace Abstraction and Abstract Interpretation (Competition Contribution).- VeriAbs : Verification by Abstraction (Competition Contribution).