


default search action
23rd TACAS 2017: Uppsala, Sweden - Part II
- 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.


Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID














