000			05473nam a22003495i 4500
001			323786
003			MX-SnUAN
005			20200810104449.0
007			cr nn 008mamaa
008			160111s2014 gw | s |||| 0|eng d
020			_a9783642548628 _9978-3-642-54862-8
035			_avtls000423515
039		9	_y201601111041 _zstaff
050		4	_aQA76.9.L63
245	1	0	_aTools and algorithms for the construction and analysis of systems : _b20th international conference, tacas 2014, held as part of the european joint conferences on theory and practice of software, etaps 2014, grenoble, france, april 5-13, 2014. Proceedings / _cedited by Erika Ábrahám, Klaus Havelund.
264		1	_aBerlin, Heidelberg : _bSpringer Berlin Heidelberg : _bSpringer, _c2014.
300			_axviii, 652 páginas : _b142 ilustraciones
336			_atexto _btxt _2rdacontent
337			_acomputadora _bc _2rdamedia
338			_arecurso en línea _bcr _2rdacarrier
347			_aarchivo de texto _bPDF _2rda
490	0		_aLecture Notes in Computer Science, _x0302-9743 ; _v8413
500			_aSpringer eBooks
505	0		_aVariations on Safety -- Decision Procedures and their Application in Analysis Decision Procedures for Flat Array Properties -- SATMC: A SAT-Based Model Checker for Security-Critical Systems -- IC3 Modulo Theories via Implicit Predicate Abstraction -- SMT-Based Verification of Software Countermeasures against Side-Channel Attacks -- Detecting Unrealizable Specifications of Distributed Systems -- Synthesizing Safe Bit-Precise Invariants -- PEALT: An Automated Reasoning Tool for Numerical Aggregation of Trust Evidence -- GRASShopper: Complete Heap Verification with Mixed Specifications -- Alternating Runtime and Size Complexity Analysis of Integer Programs -- Proving Non termination via Safety -- Ranking Templates for Linear Loops -- Modeling and Model Checking Discrete Systems FDR3 — A Modern Refinement Checker for CSP -- Concurrent Depth-First Search Algorithms -- Basic Problems in Multi-View Modeling -- GPU explore: Many-Core On-the-Fly State Space Exploration Using GPUs -- Forward Reachability Computation for Autonomous Max-Plus-Linear Systems -- Compositional Invariant Generation for Timed Systems -- Characterizing Algebraic Invariants by Differential Radical Invariants -- Quasi-Equal Clock Reduction: More Networks, More Queries -- Are Timed Automata Bad for a Specification Language? Language Inclusion Checking for Timed Automata -- Monitoring, Fault Detection and Identification Formal Design of Fault Detection and Identification Components Using Temporal Epistemic Logic -- Monitoring Modulo Theories -- Temporal-Logic Based Runtime Observer Pairs for System Health Management of Real-Time Systems -- Status Report on Software Verification (Competition Summary SV-COMP 2014) -- CBMC – C Bounded Model Checker (Competition Contribution) -- CPAchecker with Sequential Combination of Explicit-Value Analyses and Predicate Analyses (Competition Contribution) -- CPALIEN: Shape Analyzer for CPAChecker (Competition Contribution) -- Lazy-CSeq: A Lazy Sequentialization Tool for C (Competition Contribution) -- MU-CSeq: Sequentialization of C Programs by Shared Memory Unwindings (Competition Contribution) -- ESBMC 1.22 (Competition Contribution) -- FrankenBit: Bit-Precise Verification with Many Bits (Competition Contribution) -- Predator: A Shape Analyzer Based on Symbolic Memory Graphs (Competition Contribution) -- Symbiotic 2: More Precise Slicing (Competition Contribution) -- Ultimate Automizer with Unsatisfiable Cores (Competition Contribution) -- Ultimate Kojak (Competition Contribution) -- Specifying and Checking Linear Time Properties Discounting in LTL -- Symbolic Model Checking of Stutter-Invariant Properties Using Generalized Testing Automata -- Symbolic Synthesis for Epistemic Specifications with Observational Semantics -- Synthesis for Human-in-the-Loop Control Systems -- Learning Regular Languages over Large Alphabets -- Verification of Concurrent Quantum Protocols by Equivalence Checking -- Computing Conditional Probabilities in Markovian Models Efficiently -- Permissive Controller Synthesis for Probabilistic Systems -- Precise Approximations of the Probability Distribution of a Markov Process in Time: An Application to Probabilistic Invariance -- SACO: Static Analyzer for Concurrent Objects -- VeriMAP: A Tool for Verifying Programs through Transformations -- CIF 3: Model-Based Engineering of Supervisory Controllers -- EDD: A Declarative Debugger for Sequential Erlang Programs -- APTE: An Algorithm for Proving Trace Equivalence -- The Modest Toolset: An Integrated Environment for Quantitative Modelling and Verification -- Bounds2: A Tool for Compositional Multi-parametrised Verification -- On the Correctness of a Branch Displacement Algorithm -- Analyzing the Next Generation Airborne Collision Avoidance System -- Environment-Model Based Testing of Control Systems: Case Studies.
590			_aPara consulta fuera de la UANL se requiere clave de acceso remoto.
700	1		_aHavelund, Klaus, _eeditor. _9332192
710	2		_aSpringerLink (Servicio en línea) _9299170
776	0	8	_iEdición impresa: _z9783642548611
700	1		_9430263 _aÁbrahám, Erika _eeditor.
856	4	0	_uhttp://remoto.dgb.uanl.mx/login?url=http://dx.doi.org/10.1007/978-3-642-54862-8 _zConectar a Springer E-Books (Para consulta externa se requiere previa autentificación en Biblioteca Digital UANL)
942			_c14
999			_c323786 _d323786