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
Junkil Park, Miroslav Pajic, Oleg Sokolsky and Insup Lee. Automatic Verification of Finite Precision Implementations of Linear Controllers
Christel Baier, Joachim Klein, Sascha Klüppelholz and Sascha Wunderlich. Maximizing the Conditional Expected Reward for Reaching the Goal
Jan Kretinsky, Tobias Meggendorfer, Clara Waldmann and Maximilian Weininger. Index appearance record for transforming Rabin automata into parity automata
Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, Ivan Papusha, Hasan A. Poonawala and Ufuk Topcu. Sequential Convex Programming for the Efficient Verification of Parametric MDPs
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani and Tuan Phong Ngo. Context-bounded Analysis for POWER
Nima Roohi, Pavithra Prabhakar and Mahesh Viswanathan. HARE: A Hybrid Abstraction Refinement Engine for Verifying Non-Linear Hybrid Automata
Christian Schilling, Matthias Heizmann and Daniel Tischner. Minimization of Visibly Pushdown Automata Using Partial Max-SAT
Yuliya Butkova, Holger Hermanns and Ralf Wimmer. Long-run Rewards for Markov Automata
S. Akshay, Supratik Chakraborty, Ajith John, Shetal Shah. Towards Parallel Boolean Functional Synthesis
Peter Faymonville, Bernd Finkbeiner, Leander Tentrup and Markus N. Rabe. Encodings of Bounded Synthesis
Stanley Bak and Parasara Sridhar Duggirala. Rigorous Simulation-Based Analysis of Linear Hybrid Systems