Tools and Algorithms for the Construction and Analysis of Systems : 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part II - Legay, Axel.; Margaria, Tiziana; SpringerLink (Online service) (Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2017)
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). .
Keywords: Computer logic; Algorithms; Software engineering; Computers; Programming languages (Electronic computers).; Mathematical logic; Logics and Meanings of Programs; Algorithm Analysis and Problem Complexity; Software Engineering; Computation by Abstract Devices; Programming Languages, Compilers, Interpreters; Mathematical Logic and Formal Languages