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 /
| Corporate Author: | |
|---|---|
| Other Authors: | , |
| Format: | eBook |
| Language: | English |
| Published: |
Berlin, Heidelberg :
Springer Berlin Heidelberg : Imprint: Springer,
2017.
|
| Edition: | 1st ed. 2017. |
| Series: | Theoretical Computer Science and General Issues ;
10206 |
| Subjects: |
Table of Contents:
- 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). .