000 05457nam a2200433 i 4500
999 _c334640
_d334640
_x1
001 334640
003 ES-MaUEC
005 20230102114731.0
006 a|||| o|||| 10| 0
007 cr nn nnnaamaa
008 210322s2021 gw a o |1|| 0|eng d
020 _a9783030720131
024 7 _a10.1007/978-3-030-72013-1
_2doi
040 _aES-MaUEC
_bspa
_cES-MaUEC
_dES-MaUEC
050 4 _aQA76.9.S88
_b2021 EB
245 0 0 _aTools and algorithms for the construction and analysis of systems :
_b27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings
_nPart II
_cedited by Jan Friso Groote, Kim Guldstrand Larsen
250 _aFirst edition 2021
264 1 _aCham, Switzerland
_bSpringer International Publising
_c2021
300 _a1 recurso en línea (XXI, 465 páginas)
_b91 ilustraciones
336 _2rdacontent
_aTexto
_btxt
337 _2rdamedia
_aelectrónico
_bc
338 _2rdacarrier
_arecurso electrónico
_bcr
347 _atext file
_bPDF
_2rda
490 0 _aTheoretical Computer Science and General Issues
_v12652
505 0 _aVerification Techniques (not SMT) -- Directed Reachability for Infinite-State Systems -- Bridging Arrays and ADTs in Recursive Proofs -- A Two-Phase Approach for Conditional Floating-Point Verification -- Symbolic Coloured SCC Decomposition -- Case Studies -- Local Search with a SAT Oracle for Combinatorial Optimization -- Analyzing Infrastructure as Code to Prevent Intra-update Sniping Vulnerabilities -- Proof Generation/Validation -- Certifying Proofs in the First-Order Theory of Rewriting -- Syntax-Guided Quantifier Instantiation -- Making Theory Reasoning Simpler -- Deductive Stability Proofs for Ordinary Differential Equations -- Tool Papers -- An SMT-Based Approach for Verifying Binarized Neural Networks -- cake lpr: Verified Propagation Redundancy Checking in CakeML -- Deductive Veri cation of Floating-Point Java Programs in KeY -- Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types -- SyReNN: A Tool for Analyzing Deep Neural Networks -- MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers -- dtControl 2.0: Explainable Strategy Representation via Decision Tree Learning Steered by Experts -- Tool Demo Papers -- HLola: a Very Functional Tool for Extensible Stream Runtime Verification -- AMulet 2.0 for Verifying Multiplier Circuits -- RTLola on Board: Testing Real Driving Emissions on your Phone -- Replicating Restart with Prolonged Retrials: An Experimental Report -- A Web Interface for Petri Nets with Transits and Petri Games -- Momba: JANI Meets Python -- SV-Comp Tool Competition Papers -- Software Veri cation: 10th Comparative Evaluation (SV-COMP 2021) -- CPALockator: Thread-Modular Approach with Projections (Competition Contribution) -- Dartagnan: Leveraging Compiler Optimizations and the Price of Precision (Competition Contribution) -- Gazer-Theta: LLVM-based Veri er Portfolio with BMC/CEGAR (Competition Contribution) -- Goblint: Thread-Modular Abstract Interpretation Using Side-Effecting Constraints (Competition Contribution) -- Towards String Support in JayHorn (Competition Contribution) -- JDart: Portfolio Solving, Breadth-First Search and SMT-Lib Strings (Competition Contribution) -- Symbiotic 8: Beyond Symbolic Execution (Competition Contribution) -- VeriAbs: A Tool for Scalable Verification by Abstraction (Competition Contribution).
506 0 _aOpen Access
520 3 _aThis open access two-volume set constitutes the proceedings of the 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2021, which was held during March 27 - April 1, 2021, as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021. The conference was planned to take place in Luxembourg and changed to an online format due to the COVID-19 pandemic. The total of 41 full papers presented in the proceedings was carefully reviewed and selected from 141 submissions. The volume also contains 7 tool papers; 6 Tool Demo papers, 9 SV-Comp Competition Papers. The papers are organized in topical sections as follows: Part I: Game Theory; SMT Verification; Probabilities; Timed Systems; Neural Networks; Analysis of Network Communication. Part II: Verification Techniques (not SMT); Case Studies; Proof Generation/Validation; Tool Papers; Tool Demo Papers; SV-Comp Tool Competition Papers.
988 _aSpringer_Computer_2021
650 7 _2embne
_9158356
_aDiseño de sistemas
_vCongresos y asambleas
650 7 _2embne
_aAnálisis de sistemas
_vCongresos y asambleas
_9138446
700 1 _aGroote, Jan Friso
_eeditor literario
_0(orcid)0000-0003-2196-6587
_1https://orcid.org/0000-0003-2196-6587
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
700 1 _aLarsen, Kim Guldstrand
_eeditor literario
_0(orcid)0000-0002-5953-3384
_1https://orcid.org/0000-0002-5953-3384
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
710 2 _aSpringerLink
856 4 0 _uhttps://go.openathens.net/redirector/universidadeuropea.es?url=https://doi.org/10.1007/978-3-030-72013-1
_zAcceso a este recurso digital (usuarios Universidad Europea de Madrid)
942 _2lcc
_cLE
998 _b05/2021
_dz
_eb
_zSI