default search action
23rd TACAS 2017: Uppsala, Sweden (Part of ETAPS 2017)
- Axel Legay, Tiziana Margaria:
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. Lecture Notes in Computer Science 10206, 2017, ISBN 978-3-662-54579-9
Security
- Valentin Wüstholz, Oswaldo Olivo, Marijn J. H. Heule, Isil Dillig:
Static Detection of DoS Vulnerabilities in Programs that Use Regular Expressions. 3-20 - Saeid Tizpaz-Niari, Pavol Cerný, Bor-Yuh Evan Chang, Sriram Sankaranarayanan, Ashutosh Trivedi:
Discriminating Traces with Time. 21-37 - Sudipta Chattopadhyay:
Directed Automated Memory Performance Testing. 38-55 - Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Tuan Phong Ngo:
Context-Bounded Analysis for POWER. 56-74
Run-Time Verification and Logic
- Noel Brett, Umair Siddique, Borzoo Bonakdarpour:
Rewriting-Based Runtime Verification for Alternation-Free HyperLTL. 77-93 - David A. Basin, Bhargav Nagaraja Bhatt, Dmitriy Traytel:
Almost Event-Rate Independent Monitoring of Metric Temporal Logic. 94-112 - Dileep Kini, Mahesh Viswanathan:
Optimal Translation of LTL to Limit Deterministic Automata. 113-129
Quantitative Systems I
- Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, Ivan Papusha, Hasan A. Poonawala, Ufuk Topcu:
Sequential Convex Programming for the Efficient Verification of Parametric MDPs. 133-150 - Carlos E. Budde, Christian Dehnert, Ernst Moritz Hahn, Arnd Hartmanns, Sebastian Junges, Andrea Turrini:
JANI: Quantitative Model and Tool Interaction. 151-168 - Guy Avni, Shubham Goel, Thomas A. Henzinger, Guillermo Rodríguez-Navas:
Computing Scores of Forwarding Schemes in Switched Networks with Probabilistic Faults. 169-187 - Yuliya Butkova, Ralf Wimmer, Holger Hermanns:
Long-Run Rewards for Markov Automata. 188-203
SAT and SMT
- Leonardo Alt, Sepideh Asadi, Hana Chockler, Karine Even-Mendoza, Grigory Fedyukovich, Antti E. J. Hyvärinen, Natasha Sharygina:
HiFrog: SMT-based Function Summarization for Software Verification. 207-213 - Haniel Barbosa, Pascal Fontaine, Andrew Reynolds:
Congruence Closure with Free Variables. 214-230 - Roberto Sebastiani, Patrick Trentin:
On Optimization Modulo Theories, MaxSMT and Sorting Networks. 231-248 - Pedro R. G. Antonino, Thomas Gibson-Robinson, A. W. Roscoe:
The Automatic Detection of Token Structures and Invariants Using SAT Checking. 249-265
Quantitative Systems II
- Christel Baier, Joachim Klein, Sascha Klüppelholz, Sascha Wunderlich:
Maximizing the Conditional Expected Reward for Reaching the Goal. 269-285 - Anna Lukina, Lukas Esterle, Christian Hirsch, Ezio Bartocci, Junxing Yang, Ashish Tiwari, Scott A. Smolka, Radu Grosu:
ARES: Adaptive Receding-Horizon Synthesis of Optimal Plans. 286-302 - Diego Latella, Michele Loreti, Mieke Massink:
FlyFast: A Mean Field Model Checker. 303-309 - Luca Cardelli, Mirco Tribastone, Max Tschaikowski, Andrea Vandin:
ERODE: A Tool for the Evaluation and Reduction of Ordinary Differential Equations. 310-328
SV COMP
- Dirk Beyer:
Software Verification with Validation of Results - (Report on SV-COMP 2017). 331-349 - Jera Hensel, Frank Emrich, Florian Frohn, Thomas Ströder, Jürgen Giesl:
AProVE: Proving and Disproving Termination of Memory-Manipulating C Programs - (Competition Contribution). 350-354 - Pavel S. Andrianov, Karlheinz Friedberger, Mikhail U. Mandrykin, Vadim S. Mutilin, Anton Volkov:
CPA-BAM-BnB: Block-Abstraction Memoization and Region-Based Memory Models for Predicate Abstractions - (Competition Contribution). 355-359 - Williame Rocha, Herbert Rocha, Hussama Ismail, Lucas C. Cordeiro, Bernd Fischer:
DepthK: A k-Induction Verifier Based on Invariant Inference for C Programs - (Competition Contribution). 360-364 - Lukás Holík, Martin Hruska, Ondrej Lengál, Adam Rogalewicz, Jirí Simácek, Tomás Vojnar:
Forester: From Heap Shapes to Automata Predicates - (Competition Contribution). 365-369 - Ton Chanh Le, Quang-Trung Ta, Wei-Ngan Chin:
HipTNT+: A Termination and Non-termination Analyzer by Second-Order Abduction - (Competition Contribution). 370-374 - Truc L. Nguyen, Omar Inverso, Bernd Fischer, Salvatore La Torre, Gennaro Parlato:
Lazy-CSeq 2.0: Combining Lazy Sequentialization with Abstract Interpretation - (Competition Contribution). 375-379 - Franck Cassez, Anthony M. Sloane, Matthew Roberts, Matthew Pigram, Pongsak Suvanpong, Pablo González de Aledo Marugán:
Skink: Static Analysis of Programs in LLVM Intermediate Representation - (Competition Contribution). 380-384 - Marek Chalupa, Martina Vitovská, Martin Jonás, Jiri Slaby, Jan Strejcek:
Symbiotic 4: Beyond Reachability - (Competition Contribution). 385-389 - Jan Mrázek, Martin Jonás, Vladimír Still, Henrich Lauko, Jiri Barnat:
Optimizing and Caching SMT Queries in SymDIVINE - (Competition Contribution). 390-393 - Matthias Heizmann, Yu-Wen Chen, Daniel Dietsch, Marius Greitschus, Alexander Nutz, Betim Musa, Claus Schätzle, Christian Schilling, Frank Schüssele, Andreas Podelski:
Ultimate Automizer with an On-Demand Construction of Floyd-Hoare Automata - (Competition Contribution). 394-398 - Marius Greitschus, Daniel Dietsch, Matthias Heizmann, Alexander Nutz, Claus Schätzle, Christian Schilling, Frank Schüssele, Andreas Podelski:
Ultimate Taipan: Trace Abstraction and Abstract Interpretation - (Competition Contribution). 399-403 - Bharti Chimdyalwar, Priyanka Darke, Avriti Chauhan, Punit Shah, Shrawan Kumar, R. Venkatesh:
VeriAbs: Verification by Abstraction (Competition Contribution). 404-408
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.