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 I / Axel Legay, Tiziana Margaria (eds.).

Invited Talk
Validation, Synthesis and Optimization for Cyber-Physical Systems
Verification Techniques
An Abstraction Technique For Parameterized Model Checking of Leader Election Protocols: Application to FTSP
Combining String Abstract Domains for JavaScript Analysis: An Evaluation
Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF
Bounded Quantifier Instantiation for Checking Inductive Invariants
Proving Termination through Conditional Termination
Efficient Certified Resolution Proof Checking
Precise Widening Operators for Proving Termination by Abstract Interpretation
Automatic Verification of Finite Precision Implementations of Linear Controllers
Learning
Learning Symbolic Automata
ML for ML: Learning Cost Semantics by Experiment
A Novel Learning Algorithm for Büchi Automata based on Family of DFAs and Classification Trees
Synthesis
Hierarchical Network Formation Games
Synthesis of Recursive ADT Transformers from Reusable Templates
Counterexample-Guided Model Synthesis
Interpolation-Based GR(1) Assumptions Refinement
Connecting Program Synthesis and Reachability: Automatic Program Repair using Test-Input Generation
Scaling Enumerative Program Synthesis via Divide and Conquer
Towards Parallel Boolean Functional Synthesis
Encodings of Bounded Synthesis
Tools
HQSpre
An Effective Preprocessor for QBF and DQBF
RPP: Automatic Proof of Relational Properties by Self-Composition
autoCode4: Structural Controller Synthesis
Automata
Lazy Automata Techniques for WS1S
From LTL and limit-deterministic Büchi automata to deterministic parity automata
Index appearance record for transforming Rabin automata into parity automata
Minimization of Visibly Pushdown Automata Using Partial Max-SAT
Concurrency and Bisimulation
CSimpl: a Framework for the Verification of Concurrent Programs using Rely-Guarante
Fair Termination for Parameterized Probabilistic Concurrent Systems
Forward Bisimulations for Nondeterministic Symbolic Finite Automata
Up-To Techniques for Weighted Systems
Hybrid Systems
Rigorous Simulation-Based Analysis of Linear Hybrid Systems
HARE: A Hybrid Abstraction Refinement Engine for Verifying Non-Linear Hybrid Automata
Counterexample-guided Refinement of Template Polyhedra.