TACAS 2017 accepted papers

Loris D'Antoni and Margus Veanes. Forward Bisimulations for Nondeterministic Symbolic Finite Automata

Samuel Drews and Loris D'Antoni. Learning Symbolic Automata

Orna Kupferman and Tami Tamir. Hierarchical Network Formation Games

Chih-Hong Cheng, Edward Lee and Harald Ruess. autoCode4: Structural Reactive Synthesis

Ankush Das and Jan Hoffman. ML for ML: Learning Cost Semantics by Experiment

Ocan Sankur and Jean-Pierre Talpin. An Abstraction Technique For Parameterized Model Checking of Leader Election Protocols: Application to FTSP

David Sanan, Yang Liu, Zhe Hou, Yongwang Zhao, Fuyuan Zhang and Alwen Tiu. CSimpl: a Framework for the Verification of Concurrent Programs using Rely-Guarantee

Jeevana Priya Inala, Nadia Polikarpova, Xiaokang Qiu, Benjamin Lerner and Armando Solar-Lezama. Synthesis of Recursive ADT Transformers from Reusable Templates

Carlos E. Budde, Christian Dehnert, Ernst Moritz Hahn, Arnd Hartmanns, Sebastian Junges and Andrea Turrini. JANI: Quantitative Model and Tool Interaction

Noel Brett, Umair Siddique and Borzoo Bonakdarpour. Rewriting-Based Runtime Verification of Alternation-Free HyperLTL Formulas

Mathias Preiner, Aina Niemetz and Armin Biere. Counterexample-Guided Model Synthesis

Tomas Fiedor, Lukas Holik, Petr Janku, Ondrej Lengal and Tomas Vojnar. Lazy Automata Techniques for WS1S

Yotam M. Y. Feldman, Oded Padon, Neil Immerman, Mooly Sagiv and Sharon Shoham. Bounded Quantifier Instantiation for Checking Inductive Invariants

Guy Avni, Shubham Goel Shubham Goel, Thomas Henzinger and Guillermo Rodriguez-Navas. Computing Scores of Forwarding Schemes in Switched Networks with Probabilistic Faults

Ralf Wimmer, Sven Reimer, Paolo Marin and Bernd Becker. HQSpre - An Effective Preprocessor for QBF and DQBF

Leonardo Alt, Sepideh Asadi, Hana Chockler, Karine Even Mendoza, Grigory Fedyukovich, Antti Hyvärinen and Natasha Sharygina. HiFrog: SMT-based Function Summarization for Software Verification

Valentin Wuestholz, Oswaldo Olivo, Marijn Heule and Isil Dillig. Static Detection of DoS Vulnerabilities in Programs that use Regular Expressions

Roberto Amadini, Alexander Jordan, Graeme Gange, Francois Gauthier, Peter Schachte, Harald Sondergaard, Peter J. Stuckey and Chenyi Zhang. Combining String Abstract Domains for JavaScript Analysis: An Evaluation

Diego Latella, Michele Loreti and Mieke Massink. FlyFast: A Mean Field Model Checker

Javier Esparza, Jan Kretinsky, Jean-Francois Raskin and Salomon Sickert. From LTL and limit-deterministic Büchi automata to deterministic parity automata

Haniel Barbosa, Pascal Fontaine and Andrew Reynolds. Congruence Closure with Free Variables

David Basin, Bhargav Bhatt and Dmitriy Traytel. Almost Event-Rate Independent Monitoring of Metric Temporal Logic

Sergiy Bogomolov, Goran Frehse, Mirco Giacobbe and Thomas Henzinger. Counterexample-guided refinement of template polyhedra

Davide Giacomo Cavezza and Dalal Alrajeh. Interpolation-Based GR(1) Assumptions Refinement

Cristina Borralleras, Marc Brockschmidt, Daniel Larraz, Albert Oliveras, Enric Rodríguez Carbonell and Albert Rubio. Proving Termination through Conditional Termination

Luís Cruz-Filipe, Joao Marques-Silva and Peter Schneider-Kamp. Efficient Certified Resolution Proof Checking

Ondrej Lengal, Anthony Lin, Rupak Majumdar and Phillip Ruemmer. Fair Termination for Parameterized Probabilistic Concurrent Systems Anna Lukina, Lukas Esterle, Christian Hirsch, Ezio Bartocci, Junxing Yang, Ashish Tiwari, Scott A. Smolka and Radu Grosu. ARES: Adaptive Receding-Horizon Synthesis of Optimal Plans

Yong Li, Yu-Fang Chen, Lijun Zhang and Depeng Liu. A Novel Learning Algorithm for Büchi Automata based on Family of DFAs and Classification Trees

Thanhvu Nguyen, Westley Weimer, Deepak Kapur and Stephanie Forrest. Connecting Program Synthesis and Reachability: Automatic Program Repair using Test-Input Generation

Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri and Roberto Sebastiani. Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF

Roberto Sebastiani and Patrick Trentin. On Optimization Modulo Theories, MaxSMT and Sorting Networks

Rajeev Alur, Arjun Radhakrishna and Abhishek Udupa. Scaling Enumerative Program Synthesis via Divide and Conquer

Nathanaël Courant and Caterina Urban. Precise Widening Operators for Proving Termination by Abstract Interpretation

Pedro Antonino, Thomas Gibson-Robinson and Bill Roscoe. The automatic detection of token structures and invariants using SAT checking

Sebastian Küpper, Barbara König and Filippo Bonchi. Up-To Techniques for Weighted Systems Saeid Tizpaz-Niari, Pavol Cerny, Bor-Yuh Evan Chang, Sriram Sankaranarayanan and Ashutosh Trivedi. Discriminating Traces with Time

Luca Cardelli, Mirco Tribastone, Max Tschaikowski and Andrea Vandin. ERODE: A Tool for the Evaluation and Reduction of Ordinary Differential Equations

Sudipta Chattopadhyay. Directed Automated Memory Performance Testing Lionel Blatter, Nikolai Kosmatov, Virgile Prevosto and Pascale Le Gall. RPP: Automatic Proof of Relational Properties by Self-Composition

Dileep Kini and Mahesh Viswanathan. Optimal Translation of LTL to Limit Deterministic Automata