Información del autor
Autor Silva, Alexandra |
Documentos disponibles escritos por este autor (5)



27th International Workshop, WoLLIC 2021, Virtual Event, October 5–8, 2021, Proceedings / Silva, Alexandra ; Wassermann, Renata ; de Queiroz, Ruy
![]()
TÃtulo : 27th International Workshop, WoLLIC 2021, Virtual Event, October 5–8, 2021, Proceedings Tipo de documento: documento electrónico Autores: Silva, Alexandra, ; Wassermann, Renata, ; de Queiroz, Ruy, Mención de edición: 1 ed. Editorial: [s.l.] : Springer Fecha de publicación: 2021 Número de páginas: VIII, 427 p. 53 ilustraciones, 5 ilustraciones en color. ISBN/ISSN/DL: 978-3-030-88853-4 Nota general: Libro disponible en la plataforma SpringerLink. Descarga y lectura en formatos PDF, HTML y ePub. Descarga completa o por capítulos. Idioma : Inglés (eng) Palabras clave: Lógica Clasificación: 160 Lógica Resumen: Editado en colaboración con FoLLI, la Asociación de Lógica, Lenguaje e Información, este libro constituye las actas arbitradas del 27º Taller sobre Lógica, Lenguaje, Información y Comunicación, WoLLIC 2021, evento virtual, en octubre de 2021. Los 25 artÃculos completos presentados incluyeron 6 Las conferencias invitadas fueron revisadas en su totalidad y seleccionadas entre 50 presentaciones. La idea es tener un foro lo suficientemente grande en el número de interacciones posibles entre la lógica y las ciencias relacionadas con la información y la computación. Nota de contenido: Logic -- Language -- Computation -- Proofs -- Formal Languages -- Category Theory -- Deduction systems. Tipo de medio : Computadora Summary : Edited in collaboration with FoLLI, the Association of Logic, Language and Information this book constitutes the refereed proceedings of the 27th Workshop on Logic, Language, Information and Communication, WoLLIC 2021, Virtual Event, in October 2021. The 25 full papers presented included 6 invited lectures were fully reviewed and selected from 50 submissions. The idea is to have a forum which is large enough in the number of possible interactions between logic and the sciences related to information and computation. Enlace de acceso : https://link-springer-com.biblioproxy.umanizales.edu.co/referencework/10.1007/97 [...] 27th International Workshop, WoLLIC 2021, Virtual Event, October 5–8, 2021, Proceedings [documento electrónico] / Silva, Alexandra, ; Wassermann, Renata, ; de Queiroz, Ruy, . - 1 ed. . - [s.l.] : Springer, 2021 . - VIII, 427 p. 53 ilustraciones, 5 ilustraciones en color.
ISBN : 978-3-030-88853-4
Libro disponible en la plataforma SpringerLink. Descarga y lectura en formatos PDF, HTML y ePub. Descarga completa o por capítulos.
Idioma : Inglés (eng)
Palabras clave: Lógica Clasificación: 160 Lógica Resumen: Editado en colaboración con FoLLI, la Asociación de Lógica, Lenguaje e Información, este libro constituye las actas arbitradas del 27º Taller sobre Lógica, Lenguaje, Información y Comunicación, WoLLIC 2021, evento virtual, en octubre de 2021. Los 25 artÃculos completos presentados incluyeron 6 Las conferencias invitadas fueron revisadas en su totalidad y seleccionadas entre 50 presentaciones. La idea es tener un foro lo suficientemente grande en el número de interacciones posibles entre la lógica y las ciencias relacionadas con la información y la computación. Nota de contenido: Logic -- Language -- Computation -- Proofs -- Formal Languages -- Category Theory -- Deduction systems. Tipo de medio : Computadora Summary : Edited in collaboration with FoLLI, the Association of Logic, Language and Information this book constitutes the refereed proceedings of the 27th Workshop on Logic, Language, Information and Communication, WoLLIC 2021, Virtual Event, in October 2021. The 25 full papers presented included 6 invited lectures were fully reviewed and selected from 50 submissions. The idea is to have a forum which is large enough in the number of possible interactions between logic and the sciences related to information and computation. Enlace de acceso : https://link-springer-com.biblioproxy.umanizales.edu.co/referencework/10.1007/97 [...] 33rd International Conference, CAV 2021, Virtual Event, July 20–23, 2021, Proceedings, Part I / Silva, Alexandra ; Leino, K. Rustan M.
![]()
TÃtulo : 33rd International Conference, CAV 2021, Virtual Event, July 20–23, 2021, Proceedings, Part I Tipo de documento: documento electrónico Autores: Silva, Alexandra, ; Leino, K. Rustan M., Mención de edición: 1 ed. Editorial: [s.l.] : Springer Fecha de publicación: 2021 Número de páginas: XXIV, 922 p. 287 ilustraciones, 171 ilustraciones en color. ISBN/ISSN/DL: 978-3-030-81685-8 Nota general: Libro disponible en la plataforma SpringerLink. Descarga y lectura en formatos PDF, HTML y ePub. Descarga completa o por capítulos. Idioma : Inglés (eng) Palabras clave: IngenierÃa de software Inteligencia artificial Ciencias de la Computación TeorÃa de las máquinas Simulación por ordenador Lógica informática y fundamentos de la programación. Lenguajes formales y teorÃa de los autómatas Modelado por computadora Clasificación: 005.1 Resumen: Este conjunto de dos volúmenes de acceso abierto LNCS 12759 y 12760 constituye las actas arbitradas de la 33.a Conferencia Internacional sobre Verificación Asistida por Computadora, CAV 2021, celebrada virtualmente en julio de 2021. Los 63 artÃculos completos presentados junto con 16 artÃculos sobre herramientas y 5 artÃculos invitados fueron cuidadosamente revisado y seleccionado entre 290 presentaciones. Los artÃculos se organizaron en las siguientes secciones temáticas: Parte I: artÃculos invitados; Verificación de IA; concurrencia y blockchain; sistemas hÃbridos y ciberfÃsicos; seguridad; y sÃntesis. Parte II: complejidad y terminación; procedimientos de decisión y solucionadores; verificación de hardware y modelos; fundamentos lógicos; y verificación de software. Este es un libro de acceso abierto. Nota de contenido: Invited Papers -- NNrepair: Constraint-based Repair of Neural Network Classifiers -- Balancing automation and control for formal verification of microprocessors -- Algebraic Program Analysis -- Programmable Program Synthesis -- Deductive Synthesis of Programs with Pointers: Techniques, Challenges, Opportunities -- AI Verification -- DNNV: A Framework for Deep Neural Network Verification -- Robustness Verification of Quantum Classifiers -- BDD4BNN: A BDD-based Quantitative Analysis Framework for Binarized Neural Networks -- Automated Safety Verification of Programs Invoking Neural Networks -- Scalable Polyhedral Verification of Recurrent Neural Networks -- Verisig 2.0: Verification of Neural Network Controllers Using Taylor Model Preconditioning -- Robustness Verification of Semantic Segmentation Neural Networks using Relaxed Reachability -- PEREGRiNN: Penalized-Relaxation Greedy Neural Network Verifier -- Concurrency and Blockchain -- Isla: Integrating full-scale ISA semantics andaxiomatic concurrency models -- Summing Up Smart Transitions -- Stateless Model Checking under a Reads-Value-From Equivalence -- Gobra: Modular Specification and Verification of Go Programs -- Delay-Bounded Scheduling Without Delay! -- Checking Data-Race Freedom of GPU Kernels, Compositionally -- GenMC: A Model Checker for Weak Memory Models -- Hybrid and Cyber-Physical Systems -- Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming -- An Iterative Scheme of Safe Reinforcement Learning for Nonlinear Systems via Barrier Certificate Generation -- HybridSynchAADL: Modeling and Formal Analysis of Virtually Synchronous CPSs in AADL -- Computing Bottom SCCs Symbolically Using Transition Guided Reduction -- Implicit Semi-Algebraic Abstraction for Polynomial Dynamical Systems -- IMITATOR 3: Synthesis of timing parameters beyond decidability -- Formally Verified Switching Logic for Recoverability of Aircraft Controller -- SceneChecker: Boosting Scenario Verification using Symmetry Abstractions -- Effective Hybrid System Falsification Using Monte Carlo Tree Search Guided by QB-Robustness -- Fast zone-based algorithms for reachability in pushdown timed automata -- Security -- Verified Cryptographic Code for Everybody -- Not All Bugs Are Created Equal, But Robust Reachability Can Tell The Difference -- A Temporal Logic for Asynchronous Hyperproperties -- Product Programs in the Wild: Retrofitting Program Verifiers to Check Information Flow Security -- Constraint-based Relational Verification -- Pre-Deployment Security Assessment for Cloud Services through Semantic Reasoning -- Synthesis -- Synthesis with Asymptotic Resource Bounds -- Program Sketching by Automatically Generating Mocks from Tests -- Counterexample-Guided Partial Bounding for Recursive Function Synthesis -- PAYNT: A Tool for Inductive Synthesis of Probabilistic Programs -- Adapting Behaviors via Reactive Synthesis -- Causality-based Game Solving. Tipo de medio : Computadora Summary : This open access two-volume set LNCS 12759 and 12760 constitutes the refereed proceedings of the 33rd International Conference on Computer Aided Verification, CAV 2021, held virtually in July 2021. The 63 full papers presented together with 16 tool papers and 5 invited papers were carefully reviewed and selected from 290 submissions. The papers were organized in the following topical sections: Part I: invited papers; AI verification; concurrency and blockchain; hybrid and cyber-physical systems; security; and synthesis. Part II: complexity and termination; decision procedures and solvers; hardware and model checking; logical foundations; and software verification. This is an open access book. Enlace de acceso : https://link-springer-com.biblioproxy.umanizales.edu.co/referencework/10.1007/97 [...] 33rd International Conference, CAV 2021, Virtual Event, July 20–23, 2021, Proceedings, Part I [documento electrónico] / Silva, Alexandra, ; Leino, K. Rustan M., . - 1 ed. . - [s.l.] : Springer, 2021 . - XXIV, 922 p. 287 ilustraciones, 171 ilustraciones en color.
ISBN : 978-3-030-81685-8
Libro disponible en la plataforma SpringerLink. Descarga y lectura en formatos PDF, HTML y ePub. Descarga completa o por capítulos.
Idioma : Inglés (eng)
Palabras clave: IngenierÃa de software Inteligencia artificial Ciencias de la Computación TeorÃa de las máquinas Simulación por ordenador Lógica informática y fundamentos de la programación. Lenguajes formales y teorÃa de los autómatas Modelado por computadora Clasificación: 005.1 Resumen: Este conjunto de dos volúmenes de acceso abierto LNCS 12759 y 12760 constituye las actas arbitradas de la 33.a Conferencia Internacional sobre Verificación Asistida por Computadora, CAV 2021, celebrada virtualmente en julio de 2021. Los 63 artÃculos completos presentados junto con 16 artÃculos sobre herramientas y 5 artÃculos invitados fueron cuidadosamente revisado y seleccionado entre 290 presentaciones. Los artÃculos se organizaron en las siguientes secciones temáticas: Parte I: artÃculos invitados; Verificación de IA; concurrencia y blockchain; sistemas hÃbridos y ciberfÃsicos; seguridad; y sÃntesis. Parte II: complejidad y terminación; procedimientos de decisión y solucionadores; verificación de hardware y modelos; fundamentos lógicos; y verificación de software. Este es un libro de acceso abierto. Nota de contenido: Invited Papers -- NNrepair: Constraint-based Repair of Neural Network Classifiers -- Balancing automation and control for formal verification of microprocessors -- Algebraic Program Analysis -- Programmable Program Synthesis -- Deductive Synthesis of Programs with Pointers: Techniques, Challenges, Opportunities -- AI Verification -- DNNV: A Framework for Deep Neural Network Verification -- Robustness Verification of Quantum Classifiers -- BDD4BNN: A BDD-based Quantitative Analysis Framework for Binarized Neural Networks -- Automated Safety Verification of Programs Invoking Neural Networks -- Scalable Polyhedral Verification of Recurrent Neural Networks -- Verisig 2.0: Verification of Neural Network Controllers Using Taylor Model Preconditioning -- Robustness Verification of Semantic Segmentation Neural Networks using Relaxed Reachability -- PEREGRiNN: Penalized-Relaxation Greedy Neural Network Verifier -- Concurrency and Blockchain -- Isla: Integrating full-scale ISA semantics andaxiomatic concurrency models -- Summing Up Smart Transitions -- Stateless Model Checking under a Reads-Value-From Equivalence -- Gobra: Modular Specification and Verification of Go Programs -- Delay-Bounded Scheduling Without Delay! -- Checking Data-Race Freedom of GPU Kernels, Compositionally -- GenMC: A Model Checker for Weak Memory Models -- Hybrid and Cyber-Physical Systems -- Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming -- An Iterative Scheme of Safe Reinforcement Learning for Nonlinear Systems via Barrier Certificate Generation -- HybridSynchAADL: Modeling and Formal Analysis of Virtually Synchronous CPSs in AADL -- Computing Bottom SCCs Symbolically Using Transition Guided Reduction -- Implicit Semi-Algebraic Abstraction for Polynomial Dynamical Systems -- IMITATOR 3: Synthesis of timing parameters beyond decidability -- Formally Verified Switching Logic for Recoverability of Aircraft Controller -- SceneChecker: Boosting Scenario Verification using Symmetry Abstractions -- Effective Hybrid System Falsification Using Monte Carlo Tree Search Guided by QB-Robustness -- Fast zone-based algorithms for reachability in pushdown timed automata -- Security -- Verified Cryptographic Code for Everybody -- Not All Bugs Are Created Equal, But Robust Reachability Can Tell The Difference -- A Temporal Logic for Asynchronous Hyperproperties -- Product Programs in the Wild: Retrofitting Program Verifiers to Check Information Flow Security -- Constraint-based Relational Verification -- Pre-Deployment Security Assessment for Cloud Services through Semantic Reasoning -- Synthesis -- Synthesis with Asymptotic Resource Bounds -- Program Sketching by Automatically Generating Mocks from Tests -- Counterexample-Guided Partial Bounding for Recursive Function Synthesis -- PAYNT: A Tool for Inductive Synthesis of Probabilistic Programs -- Adapting Behaviors via Reactive Synthesis -- Causality-based Game Solving. Tipo de medio : Computadora Summary : This open access two-volume set LNCS 12759 and 12760 constitutes the refereed proceedings of the 33rd International Conference on Computer Aided Verification, CAV 2021, held virtually in July 2021. The 63 full papers presented together with 16 tool papers and 5 invited papers were carefully reviewed and selected from 290 submissions. The papers were organized in the following topical sections: Part I: invited papers; AI verification; concurrency and blockchain; hybrid and cyber-physical systems; security; and synthesis. Part II: complexity and termination; decision procedures and solvers; hardware and model checking; logical foundations; and software verification. This is an open access book. Enlace de acceso : https://link-springer-com.biblioproxy.umanizales.edu.co/referencework/10.1007/97 [...] 33rd International Conference, CAV 2021, Virtual Event, July 20–23, 2021, Proceedings, Part II / Silva, Alexandra ; Leino, K. Rustan M.
![]()
TÃtulo : 33rd International Conference, CAV 2021, Virtual Event, July 20–23, 2021, Proceedings, Part II Tipo de documento: documento electrónico Autores: Silva, Alexandra, ; Leino, K. Rustan M., Mención de edición: 1 ed. Editorial: [s.l.] : Springer Fecha de publicación: 2021 Número de páginas: XXIII, 940 p. 382 ilustraciones, 234 ilustraciones en color. ISBN/ISSN/DL: 978-3-030-81688-9 Nota general: Libro disponible en la plataforma SpringerLink. Descarga y lectura en formatos PDF, HTML y ePub. Descarga completa o por capítulos. Idioma : Inglés (eng) Palabras clave: IngenierÃa de software TeorÃa de las máquinas Inteligencia artificial Ciencias de la Computación Simulación por ordenador Lenguajes formales y teorÃa de los autómatas Lógica informática y fundamentos de la programación. Modelado por computadora Clasificación: 005.1 Resumen: Este conjunto de dos volúmenes de acceso abierto LNCS 12759 y 12760 constituye las actas arbitradas de la 33.a Conferencia Internacional sobre Verificación Asistida por Computadora, CAV 2021, celebrada virtualmente en julio de 2021. Los 63 artÃculos completos presentados junto con 16 artÃculos sobre herramientas y 5 artÃculos invitados fueron cuidadosamente revisado y seleccionado entre 290 presentaciones. Los artÃculos se organizaron en las siguientes secciones temáticas: Parte I: artÃculos invitados; Verificación de IA; concurrencia y blockchain; sistemas hÃbridos y ciberfÃsicos; seguridad; y sÃntesis. Parte II: complejidad y terminación; procedimientos de decisión y solucionadores; verificación de hardware y modelos; fundamentos lógicos; y verificación de software. Nota de contenido: Complexity and Termination -- Learning Probabilistic Termination Proofs -- Ghost Signals: Verifying Termination of Busy Waiting -- Reflections on Termination of Linear Loops -- Decision Tree Learning in CEGIS-Based Termination Analysis -- ATLAS: Automated Amortised Complexity Analysis of Self-Adjusting Data Structures -- Decision Procedures and Solvers -- Theory Exploration Powered by Deductive Synthesis -- CoqQFBV: A Scalable Certified SMT Quantifier-Free Bit-Vector Solver -- Porous Invariants -- JavaSMT 3: Interacting with SMT Solvers in Java -- Efficient SMT-based Analysis of Failure Propagation -- ToolX : Better Delta Debugging for the SMT-LIBv2 Language and Friends -- Learning Union of Integer Hypercubes with Queries (with applications to monadic decomposition) -- Interpolation and Model Checking for Nonlinear Arithmetic -- An SMT Solver for Regular Expressions and Linear Arithmetic over String Length -- Counting Minimal Unsatisfiable Subsets -- Sound Verification Procedures for Temporal Properties of Infinite-State Systems -- Hardware and Model Checking -- Progress in Certifying Hardware Model Checking Results -- Model-Checking Structured Context-Free Languages -- Model Checking ! -Regular Properties with Decoupled Search -- AIGEN: Random Generation of Symbolic Transition Systems -- GPU Acceleration of Bounded Model Checking with ParaFROST -- Pono: A Flexible and Extensible SMT-based Model Checker -- Logical Foundations -- Towards a Trustworthy Semantics-Based Language Framework via Proof Generation -- Formal Foundations of Fine-Grained Explainability -- Latticed k-Induction with an Application to Probabilistic Programs -- Stochastic Systems -- Runtime Monitors for Markov Decision Processes -- Model Checking Finite-Horizon Markov Chains with Probabilistic Inference -- Enforcing Almost-Sure Reachability in POMDPs -- Rigorous Floating-Point Roundo Error Analysis of Probabilistic Computations -- Model-free Reinforcement Learning for Branching Markov Decision Processes -- Software Verification -- Cameleer: a Deductive Verification Tool for OCaml -- LLMC: Verifying High-Performance Software -- Formally Validating a Practical Verification Condition Generator -- Automatic Generation and Validation of Instruction Encoders and Decoders -- An SMT Encoding of LLVM's Memory Model for Bounded Translation Validation -- Automatically Tailoring Abstract Interpretation to Custom Usage Scenarios -- Functional Correctness of C implementations of Dijkstra's, Kruskal's, and Prim's Algorithms -- Gillian, Part II: Real-World Verification for JavaScript and C -- Debugging Network Reachability with Blocked Paths -- Lower-Bound Synthesis using Loop Specialization and Max-SMT -- Fast Computation of Strong Control Dependencies -- Di y: Inductive Reasoning of Array Programs using Difference Invariants. Tipo de medio : Computadora Summary : This open access two-volume set LNCS 12759 and 12760 constitutes the refereed proceedings of the 33rd International Conference on Computer Aided Verification, CAV 2021, held virtually in July 2021. The 63 full papers presented together with 16 tool papers and 5 invited papers were carefully reviewed and selected from 290 submissions. The papers were organized in the following topical sections: Part I: invited papers; AI verification; concurrency and blockchain; hybrid and cyber-physical systems; security; and synthesis. Part II: complexity and termination; decision procedures and solvers; hardware and model checking; logical foundations; and software verification. Enlace de acceso : https://link-springer-com.biblioproxy.umanizales.edu.co/referencework/10.1007/97 [...] 33rd International Conference, CAV 2021, Virtual Event, July 20–23, 2021, Proceedings, Part II [documento electrónico] / Silva, Alexandra, ; Leino, K. Rustan M., . - 1 ed. . - [s.l.] : Springer, 2021 . - XXIII, 940 p. 382 ilustraciones, 234 ilustraciones en color.
ISBN : 978-3-030-81688-9
Libro disponible en la plataforma SpringerLink. Descarga y lectura en formatos PDF, HTML y ePub. Descarga completa o por capítulos.
Idioma : Inglés (eng)
Palabras clave: IngenierÃa de software TeorÃa de las máquinas Inteligencia artificial Ciencias de la Computación Simulación por ordenador Lenguajes formales y teorÃa de los autómatas Lógica informática y fundamentos de la programación. Modelado por computadora Clasificación: 005.1 Resumen: Este conjunto de dos volúmenes de acceso abierto LNCS 12759 y 12760 constituye las actas arbitradas de la 33.a Conferencia Internacional sobre Verificación Asistida por Computadora, CAV 2021, celebrada virtualmente en julio de 2021. Los 63 artÃculos completos presentados junto con 16 artÃculos sobre herramientas y 5 artÃculos invitados fueron cuidadosamente revisado y seleccionado entre 290 presentaciones. Los artÃculos se organizaron en las siguientes secciones temáticas: Parte I: artÃculos invitados; Verificación de IA; concurrencia y blockchain; sistemas hÃbridos y ciberfÃsicos; seguridad; y sÃntesis. Parte II: complejidad y terminación; procedimientos de decisión y solucionadores; verificación de hardware y modelos; fundamentos lógicos; y verificación de software. Nota de contenido: Complexity and Termination -- Learning Probabilistic Termination Proofs -- Ghost Signals: Verifying Termination of Busy Waiting -- Reflections on Termination of Linear Loops -- Decision Tree Learning in CEGIS-Based Termination Analysis -- ATLAS: Automated Amortised Complexity Analysis of Self-Adjusting Data Structures -- Decision Procedures and Solvers -- Theory Exploration Powered by Deductive Synthesis -- CoqQFBV: A Scalable Certified SMT Quantifier-Free Bit-Vector Solver -- Porous Invariants -- JavaSMT 3: Interacting with SMT Solvers in Java -- Efficient SMT-based Analysis of Failure Propagation -- ToolX : Better Delta Debugging for the SMT-LIBv2 Language and Friends -- Learning Union of Integer Hypercubes with Queries (with applications to monadic decomposition) -- Interpolation and Model Checking for Nonlinear Arithmetic -- An SMT Solver for Regular Expressions and Linear Arithmetic over String Length -- Counting Minimal Unsatisfiable Subsets -- Sound Verification Procedures for Temporal Properties of Infinite-State Systems -- Hardware and Model Checking -- Progress in Certifying Hardware Model Checking Results -- Model-Checking Structured Context-Free Languages -- Model Checking ! -Regular Properties with Decoupled Search -- AIGEN: Random Generation of Symbolic Transition Systems -- GPU Acceleration of Bounded Model Checking with ParaFROST -- Pono: A Flexible and Extensible SMT-based Model Checker -- Logical Foundations -- Towards a Trustworthy Semantics-Based Language Framework via Proof Generation -- Formal Foundations of Fine-Grained Explainability -- Latticed k-Induction with an Application to Probabilistic Programs -- Stochastic Systems -- Runtime Monitors for Markov Decision Processes -- Model Checking Finite-Horizon Markov Chains with Probabilistic Inference -- Enforcing Almost-Sure Reachability in POMDPs -- Rigorous Floating-Point Roundo Error Analysis of Probabilistic Computations -- Model-free Reinforcement Learning for Branching Markov Decision Processes -- Software Verification -- Cameleer: a Deductive Verification Tool for OCaml -- LLMC: Verifying High-Performance Software -- Formally Validating a Practical Verification Condition Generator -- Automatic Generation and Validation of Instruction Encoders and Decoders -- An SMT Encoding of LLVM's Memory Model for Bounded Translation Validation -- Automatically Tailoring Abstract Interpretation to Custom Usage Scenarios -- Functional Correctness of C implementations of Dijkstra's, Kruskal's, and Prim's Algorithms -- Gillian, Part II: Real-World Verification for JavaScript and C -- Debugging Network Reachability with Blocked Paths -- Lower-Bound Synthesis using Loop Specialization and Max-SMT -- Fast Computation of Strong Control Dependencies -- Di y: Inductive Reasoning of Array Programs using Difference Invariants. Tipo de medio : Computadora Summary : This open access two-volume set LNCS 12759 and 12760 constitutes the refereed proceedings of the 33rd International Conference on Computer Aided Verification, CAV 2021, held virtually in July 2021. The 63 full papers presented together with 16 tool papers and 5 invited papers were carefully reviewed and selected from 290 submissions. The papers were organized in the following topical sections: Part I: invited papers; AI verification; concurrency and blockchain; hybrid and cyber-physical systems; security; and synthesis. Part II: complexity and termination; decision procedures and solvers; hardware and model checking; logical foundations; and software verification. Enlace de acceso : https://link-springer-com.biblioproxy.umanizales.edu.co/referencework/10.1007/97 [...] Formal Techniques for Distributed Objects, Components, and Systems / Bouajjani, Ahmed ; Silva, Alexandra
![]()
TÃtulo : Formal Techniques for Distributed Objects, Components, and Systems : 37th IFIP WG 6.1 International Conference, FORTE 2017, Held as Part of the 12th International Federated Conference on Distributed Computing Techniques, DisCoTec 2017, Neuchâtel, Switzerland, June 19-22, 2017, Proceedings Tipo de documento: documento electrónico Autores: Bouajjani, Ahmed, ; Silva, Alexandra, Mención de edición: 1 ed. Editorial: [s.l.] : Springer Fecha de publicación: 2017 Número de páginas: XIV, 243 p. 50 ilustraciones ISBN/ISSN/DL: 978-3-319-60225-7 Nota general: Libro disponible en la plataforma SpringerLink. Descarga y lectura en formatos PDF, HTML y ePub. Descarga completa o por capítulos. Idioma : Inglés (eng) Palabras clave: Ciencias de la Computación IngenierÃa de software Inteligencia artificial TeorÃa de las máquinas Red de computadoras Lógica informática y fundamentos de la programación. Lenguajes formales y teorÃa de los autómatas Redes de comunicación informática Clasificación: 40.151 Resumen: Este libro constituye las actas de la 37.ª Conferencia Internacional IFIP WG 6.1 sobre Técnicas Formales para Objetos, Componentes y Sistemas Distribuidos, FORTE 2017, celebrada en Neuchâtel, Suiza, en junio de 2017, como parte de la 12.ª Conferencia Federada Internacional sobre Técnicas de Computación Distribuida. , DisCoTec 2017. Los 13 artÃculos completos revisados ​​presentados junto con 3 artÃculos breves y 1 artÃculo de herramientas fueron cuidadosamente revisados ​​y seleccionados entre 30 presentaciones. Los artÃculos presentan una amplia gama de temas sobre modelos de computación distribuida y métodos formales de especificación, prueba y verificación. Nota de contenido: Session types for Link failures -- Learning-based compositional parameter synthesis for event-recording automata -- Modularising opacity verification for Hybrid Transactional Memory -- Proving opacity via linearizability: a sound and complete method -- On futures for streaming data in ABS -- Session-based concurrency, reactively -- Procedural choreographic programming -- An observational approach to defining linearizability on weak memory models -- Applying a dependency mechanism in the formal development of voting protocol models using event-B -- Weak simulation quasimetric in a gossip scenario -- Reasoning about distributed secrets -- Classical higher-order processes -- Weak nominal modal logic -- Type inference of simulink hierarchical block diagrams in Isabelle -- Creating Büchi automata for multi-valued model checking -- Privacy assessment using static taint analysis -- EPTL - a temporal logic for weakly consistent systems. Tipo de medio : Computadora Summary : This book constitutes the proceedings of the 37th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2017, held in Neuchâtel, Switzerland, in June 2017, as part of the 12th International Federated Conference on Distributed Computing Techniques, DisCoTec 2017. The 13 revised full papers presented together with 3 short and 1 tool papers were carefully reviewed and selected from 30 submissions. The papers present a wide range of topics on distributed computing models and formal specification, testing, and verification methods. Enlace de acceso : https://link-springer-com.biblioproxy.umanizales.edu.co/referencework/10.1007/97 [...] Formal Techniques for Distributed Objects, Components, and Systems : 37th IFIP WG 6.1 International Conference, FORTE 2017, Held as Part of the 12th International Federated Conference on Distributed Computing Techniques, DisCoTec 2017, Neuchâtel, Switzerland, June 19-22, 2017, Proceedings [documento electrónico] / Bouajjani, Ahmed, ; Silva, Alexandra, . - 1 ed. . - [s.l.] : Springer, 2017 . - XIV, 243 p. 50 ilustraciones.
ISBN : 978-3-319-60225-7
Libro disponible en la plataforma SpringerLink. Descarga y lectura en formatos PDF, HTML y ePub. Descarga completa o por capítulos.
Idioma : Inglés (eng)
Palabras clave: Ciencias de la Computación IngenierÃa de software Inteligencia artificial TeorÃa de las máquinas Red de computadoras Lógica informática y fundamentos de la programación. Lenguajes formales y teorÃa de los autómatas Redes de comunicación informática Clasificación: 40.151 Resumen: Este libro constituye las actas de la 37.ª Conferencia Internacional IFIP WG 6.1 sobre Técnicas Formales para Objetos, Componentes y Sistemas Distribuidos, FORTE 2017, celebrada en Neuchâtel, Suiza, en junio de 2017, como parte de la 12.ª Conferencia Federada Internacional sobre Técnicas de Computación Distribuida. , DisCoTec 2017. Los 13 artÃculos completos revisados ​​presentados junto con 3 artÃculos breves y 1 artÃculo de herramientas fueron cuidadosamente revisados ​​y seleccionados entre 30 presentaciones. Los artÃculos presentan una amplia gama de temas sobre modelos de computación distribuida y métodos formales de especificación, prueba y verificación. Nota de contenido: Session types for Link failures -- Learning-based compositional parameter synthesis for event-recording automata -- Modularising opacity verification for Hybrid Transactional Memory -- Proving opacity via linearizability: a sound and complete method -- On futures for streaming data in ABS -- Session-based concurrency, reactively -- Procedural choreographic programming -- An observational approach to defining linearizability on weak memory models -- Applying a dependency mechanism in the formal development of voting protocol models using event-B -- Weak simulation quasimetric in a gossip scenario -- Reasoning about distributed secrets -- Classical higher-order processes -- Weak nominal modal logic -- Type inference of simulink hierarchical block diagrams in Isabelle -- Creating Büchi automata for multi-valued model checking -- Privacy assessment using static taint analysis -- EPTL - a temporal logic for weakly consistent systems. Tipo de medio : Computadora Summary : This book constitutes the proceedings of the 37th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2017, held in Neuchâtel, Switzerland, in June 2017, as part of the 12th International Federated Conference on Distributed Computing Techniques, DisCoTec 2017. The 13 revised full papers presented together with 3 short and 1 tool papers were carefully reviewed and selected from 30 submissions. The papers present a wide range of topics on distributed computing models and formal specification, testing, and verification methods. Enlace de acceso : https://link-springer-com.biblioproxy.umanizales.edu.co/referencework/10.1007/97 [...]
TÃtulo : Language, Logic, and Computation : 12th International Tbilisi Symposium, TbiLLC 2017, Lagodekhi, Georgia, September 18-22, 2017, Revised Selected Papers Tipo de documento: documento electrónico Autores: Silva, Alexandra, ; Staton, Sam, ; Sutton, Peter, ; Umbach, Carla, Mención de edición: 1 ed. Editorial: Berlin [Alemania] : Springer Fecha de publicación: 2019 Número de páginas: XIV, 353 p. 294 ilustraciones, 6 ilustraciones en color. ISBN/ISSN/DL: 978-3-662-59565-7 Nota general: Libro disponible en la plataforma SpringerLink. Descarga y lectura en formatos PDF, HTML y ePub. Descarga completa o por capítulos. Idioma : Inglés (eng) Palabras clave: TeorÃa de las máquinas Programación lógica Informática Estadistica matematica Lenguajes formales y teorÃa de los autómatas Lógica en IA Probabilidad y EstadÃstica en Informática Clasificación: 5.131 Resumen: Este libro constituye las actas arbitradas del 12.° Simposio Internacional de Tbilisi sobre Lógica, Lenguaje y Computación, TbiLLC 2017, celebrado en Lagodekhi, Georgia, en septiembre de 2017. El volumen contiene 17 artÃculos completos revisados ​​presentados en la conferencia a partir de 22 presentaciones. El objetivo de esta serie de conferencias es reunir a investigadores de una amplia variedad de campos en sintaxis del lenguaje natural, tipologÃa lingüÃstica, evolución del lenguaje, lógica para la inteligencia artificial y mucho más. . Nota de contenido: Compounds or Phrases? Pattern Borrowing from English into Georgian -- A Study of Subminimal Logics of Negation and their Modal Companions -- Finite identification with positive and with complete data -- Two Neighborhood Semantics for Subintuitionistic Logics -- Bare nouns and the Hungarian mass/count distinction -- Why aktionsart-based event structure templates are not enough – A frame account of leaking and droning -- The athlete tore a muscle: English Locative Subjects in the Extra Argument Construction -- An Axiomatization of the d-logic of Planar Polygons -- An Ehrenfeucht–Fraisse game for inquisitive first-order logic -- Computational Model of the Modern Georgian Language and Search Patterns for an Online Dictionary of Idioms -- Language as Mechanisms for Interaction: Towards An Evolutionary Tale -- Bridging inferences in a dynamic frame theory -- Misfits: On unexpected German ob-predicates -- A Non-factualist Semantics for Attributions of Comparative Value -- Spectra of Goedel Algebras -- From Semantic Memory to Semantic Content -- Explaining meaning: The interplay of syntax, semantics, and pragmatics. Tipo de medio : Computadora Summary : This book constitutes the refereed proceedings of the 12th International Tbilisi Symposium on Logic, Language and Computation, TbiLLC 2017, held in Lagodekhi, Georgia, in September 2017. The volume contains 17 full revised papers presented at the conference from 22 submissions. The aim of this conference series is to bring together researchers from a wide variety of fields in Natural language syntax, Linguistic typology, Language evolution, Logics for artificial intelligence and much more. . Enlace de acceso : https://link-springer-com.biblioproxy.umanizales.edu.co/referencework/10.1007/97 [...] Language, Logic, and Computation : 12th International Tbilisi Symposium, TbiLLC 2017, Lagodekhi, Georgia, September 18-22, 2017, Revised Selected Papers [documento electrónico] / Silva, Alexandra, ; Staton, Sam, ; Sutton, Peter, ; Umbach, Carla, . - 1 ed. . - Berlin [Alemania] : Springer, 2019 . - XIV, 353 p. 294 ilustraciones, 6 ilustraciones en color.
ISBN : 978-3-662-59565-7
Libro disponible en la plataforma SpringerLink. Descarga y lectura en formatos PDF, HTML y ePub. Descarga completa o por capítulos.
Idioma : Inglés (eng)
Palabras clave: TeorÃa de las máquinas Programación lógica Informática Estadistica matematica Lenguajes formales y teorÃa de los autómatas Lógica en IA Probabilidad y EstadÃstica en Informática Clasificación: 5.131 Resumen: Este libro constituye las actas arbitradas del 12.° Simposio Internacional de Tbilisi sobre Lógica, Lenguaje y Computación, TbiLLC 2017, celebrado en Lagodekhi, Georgia, en septiembre de 2017. El volumen contiene 17 artÃculos completos revisados ​​presentados en la conferencia a partir de 22 presentaciones. El objetivo de esta serie de conferencias es reunir a investigadores de una amplia variedad de campos en sintaxis del lenguaje natural, tipologÃa lingüÃstica, evolución del lenguaje, lógica para la inteligencia artificial y mucho más. . Nota de contenido: Compounds or Phrases? Pattern Borrowing from English into Georgian -- A Study of Subminimal Logics of Negation and their Modal Companions -- Finite identification with positive and with complete data -- Two Neighborhood Semantics for Subintuitionistic Logics -- Bare nouns and the Hungarian mass/count distinction -- Why aktionsart-based event structure templates are not enough – A frame account of leaking and droning -- The athlete tore a muscle: English Locative Subjects in the Extra Argument Construction -- An Axiomatization of the d-logic of Planar Polygons -- An Ehrenfeucht–Fraisse game for inquisitive first-order logic -- Computational Model of the Modern Georgian Language and Search Patterns for an Online Dictionary of Idioms -- Language as Mechanisms for Interaction: Towards An Evolutionary Tale -- Bridging inferences in a dynamic frame theory -- Misfits: On unexpected German ob-predicates -- A Non-factualist Semantics for Attributions of Comparative Value -- Spectra of Goedel Algebras -- From Semantic Memory to Semantic Content -- Explaining meaning: The interplay of syntax, semantics, and pragmatics. Tipo de medio : Computadora Summary : This book constitutes the refereed proceedings of the 12th International Tbilisi Symposium on Logic, Language and Computation, TbiLLC 2017, held in Lagodekhi, Georgia, in September 2017. The volume contains 17 full revised papers presented at the conference from 22 submissions. The aim of this conference series is to bring together researchers from a wide variety of fields in Natural language syntax, Linguistic typology, Language evolution, Logics for artificial intelligence and much more. . Enlace de acceso : https://link-springer-com.biblioproxy.umanizales.edu.co/referencework/10.1007/97 [...]