000 05733nam a22006135i 4500
001 978-3-662-54577-5
003 DE-He213
005 20240730184243.0
007 cr nn 008mamaa
008 170330s2017 gw | s |||| 0|eng d
020 _a9783662545775
_9978-3-662-54577-5
024 7 _a10.1007/978-3-662-54577-5
_2doi
050 4 _aQA75.5-76.95
072 7 _aUYA
_2bicssc
072 7 _aCOM014000
_2bisacsh
072 7 _aUYA
_2thema
082 0 4 _a004.0151
_223
245 1 0 _aTools and Algorithms for the Construction and Analysis of Systems
_h[electronic resource] :
_b23rd 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 /
_cedited by Axel Legay, Tiziana Margaria.
250 _a1st ed. 2017.
264 1 _aBerlin, Heidelberg :
_bSpringer Berlin Heidelberg :
_bImprint: Springer,
_c2017.
300 _aXXIV, 609 p. 152 illus.
_bonline resource.
336 _atext
_btxt
_2rdacontent
337 _acomputer
_bc
_2rdamedia
338 _aonline resource
_bcr
_2rdacarrier
347 _atext file
_bPDF
_2rda
490 1 _aTheoretical Computer Science and General Issues,
_x2512-2029 ;
_v10205
505 0 _aInvited 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 fromReusable 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. .
520 _aThe two-book set LNCS 10205 + 10206 constitutes the proceedings of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2017, which took place in Uppsala, Sweden in April 2017, held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017. The 48 full papers, 4 tool demonstration papers, and 12 software competition papers presented in these volumes were carefully reviewed and selected from 181 submissions to TACAS and 32 submissions to the software competition. They were organized in topical sections named: verification techniques; learning; synthesis; automata; concurrency and bisimulation; hybrid systems; security; run-time verification and logic; quantitative systems; SAT and SMT; and SV COMP. .
650 0 _aComputer science.
_99832
650 0 _aAlgorithms.
_93390
650 0 _aSoftware engineering.
_94138
650 0 _aCompilers (Computer programs).
_93350
650 0 _aMachine theory.
_9135044
650 1 4 _aComputer Science Logic and Foundations of Programming.
_942203
650 2 4 _aAlgorithms.
_93390
650 2 4 _aSoftware Engineering.
_94138
650 2 4 _aTheory of Computation.
_9135045
650 2 4 _aCompilers and Interpreters.
_931853
650 2 4 _aFormal Languages and Automata Theory.
_9135046
700 1 _aLegay, Axel.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
_9135047
700 1 _aMargaria, Tiziana.
_eeditor.
_0(orcid)
_10000-0002-5547-9739
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
_9135048
710 2 _aSpringerLink (Online service)
_9135049
773 0 _tSpringer Nature eBook
776 0 8 _iPrinted edition:
_z9783662545768
776 0 8 _iPrinted edition:
_z9783662545782
830 0 _aTheoretical Computer Science and General Issues,
_x2512-2029 ;
_v10205
_9135050
856 4 0 _uhttps://doi.org/10.1007/978-3-662-54577-5
912 _aZDB-2-SCS
912 _aZDB-2-SXCS
912 _aZDB-2-LNC
942 _cELN
999 _c92260
_d92260