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 /
| Autor Corporativo: | |
|---|---|
| Otros Autores: | , |
| Formato: | eBook |
| Lenguaje: | English |
| Publicado: |
Berlin, Heidelberg :
Springer Berlin Heidelberg : Imprint: Springer,
2017.
|
| Edición: | 1st ed. 2017. |
| Colección: | Theoretical Computer Science and General Issues ;
10205 |
| Materias: |
Tabla de Contenidos:
- 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 Buchi 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. .