{"text_format":"2","workbook":"xls","n_sheets":1,"sheets":["report2"],"not_rendered":{"charts":0,"images":0,"macros":0,"external_links":1,"defined_names":2,"comments":0,"pivot_tables":0},"unopened":[],"bounds":{"document_bytes":16777216,"sheet_cells":100000,"run_cost":"one","rows_first":2000,"rows_last":500,"rows_between":2000,"halvings":0,"cell_chars":16384,"cell_head_chars":4096},"cells_cut":0,"cells_raw":0,"read":"whole","date_system":"1900","formulas":"cached_only"}

{"sheet":"report2","index":0,"n_rows":44,"n_cols":5,"rows_kept":44,"cut":false,"hidden":false,"merged":[[0,2,0,3],[0,4,0,5],[1,2,1,3],[1,4,1,5],[2,2,2,3],[4,2,4,3],[5,2,5,3],[6,2,6,3],[7,2,7,3],[8,2,8,3],[9,2,9,3],[11,2,11,3],[12,2,12,3],[16,2,16,3],[19,2,19,3],[19,4,19,5],[20,2,20,3],[20,4,20,5],[21,2,21,3],[21,4,21,5],[22,2,22,3],[23,2,23,3],[25,2,25,3],[26,2,26,3],[27,2,27,3],[28,2,28,3],[29,2,29,3],[38,2,38,3],[39,2,39,3],[41,2,41,3]],"flags":["formulas_cached_only"]}
[null,"1.","Record Nr.",null,"UNINA9910143460703321"]
[null,null,"Titolo",null,"Computer-aided verification : 11th International Conference, Cav '99, Trento, Italy, July 6-1-10, 1999 : proceedings / / Nicolas Halbwachs, Doron Peled (editors)"]
[null,null,"Pubbl/distr/stampa",null,"Berlin : , : Springer, , [1999]"]
[{"$nulls":4},"Â©1999"]
[null,null,"ISBN",null,"3-540-48683-6"]
[null,null,"Edizione",null,"[1st ed. 1999.]"]
[null,null,"Descrizione fisica",null,"1 online resource (XIV, 506 p.)"]
[null,null,"Collana",null,"Lecture notes in computer science ; ; 1633"]
[null,null,"Disciplina",null,"005.14"]
[null,null,"Soggetti",null,"Computer software - Verification"]
[{"$nulls":4},"Electronic digital computers - Evaluation"]
[null,null,"Lingua di pubblicazione",null,"Inglese"]
[null,null,"Formato",null,"Materiale a stampa"]
[null,null,null,"Livello bibliografico","Monografia"]
[null,null,null,"Note generali","Bibliographic Level Mode of Issuance: Monograph"]
[null,null,null,"Nota di bibliografia","Includes bibliographical references and index."]
[null,null,"Nota di contenuto",null,"Tutorials and Invited Papers -- Alternative Approaches to Hardware Verification -- The Compositional Specification of Timed Systems — A Tutorial -- Timed Automata -- Ståalmarck’s Method with Extensions to Quantified Boolean Formulas -- Verification of Parameterized Systems by Dynamic Induction -- Formal Methods for Conformance Testing: Theory Can Be Practical -- Processor Verification -- Proof of Correctness of a Processor with Reorder Buffer Using the Completion Functions Approach -- Verifying Safety Properties of a PowerPC? Microprocessor Using Symbolic Model Checking without BDDs -- Model Checking the IBM Gigahertz Processor: An Abstraction Algorithm for High-Performance Netlists -- Validation of Pipelined Processor Designs Using Esterel Tools: A Case Study -- Protocol Verification and Testing -- Automated Verification of a Parametric Real-Time Program: The ABR Conformance Protocol -- Test Generation Derived from Model-Checking -- Latency Insensitive Protocols -- Infinite State Space -- Handling Global Conditions in Parametrized System Verification -- Verification of Infinite-State Systems by Combining Abstraction and Reachability Analysis -- Experience with Predicate Abstraction -- Theory of Verification -- Model Checking of Safety Properties -- A Complete Finite Prefix for Process Algebra -- The Mathematical Foundation of Symbolic Trajectory Evaluation -- Assume-Guarantee Refinement between Different Time Scales -- Linear Temporal Logic -- Efficient Decision Procedures for Model Checking of Linear Time Logic "]
[{"$nulls":4},"Properties -- Stutter-Invariant Languages, ?-Automata, and Temporal Logic -- Improved Automata Generation for Linear Temporal Logic -- Modeling of Systems -- On the Representation of Probabilities over Structured Domains -- Model Checking Partial State Spaces with 3-Valued Temporal Logics -- Elementary Microarchitecture Algebra -- Verifying Sequential Consistency on Shared-Memory Multiprocessor Systems -- Symbolic Model-Checking -- Stepwise CTL Model Checking of State/Event Systems -- Optimizing Symbolic Model Checking for Constraint-Rich Models -- Efficient Timed Reachability Analysis Using Clock Difference Diagrams -- Theorem Proving -- Mechanizing Proofs of Computation Equivalence -- Linking Theorem Proving and Model-Checking with Well-Founded Bisimulation -- Automatic Verification of Combinational and Pipelined FFT Circuits -- Automata-Theoretic Methods -- Efficient Analysis of Cyclic Definitions -- A Theory of Restrictions for Logics and Automata -- Model Checking Based on Sequential ATPG -- Automatic Verification of Abstract State Machines -- Abstraction -- Abstract and Model Check while You Prove -- Deciding Equality Formulas by Small Domains Instantiations -- Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions -- Tool Presentations -- A Toolbox for the Analysis of Discrete Event Dynamic Systems -- TIPPtool: Compositional Specification and Analysis of Markovian Performance Models -- Java Bytecode Verification by Model Checking -- NuSMV: A New Symbolic Model Verifier -- PIL/SETHEO: A Tool for the Automatic Analysis of Authentication Protocols."]
[null,null,null,"Sommario/riassunto","This book constitutes the refereed proceedings of the 11th International Conference on Computer Aided Verification, CAV'99, held in Trento, Italy in July 1999 as part of FLoC'99. The 34 revised full papers presented were carefully reviewed and selected from a total of 107 submissions. Also included are six invited contributions and five tool presentations. The book is organized in topical sections on processor verification, protocol verification and testing, infinite state spaces, theory of verification, linear temporal logic, modeling of systems, symbolic model checking, theorem proving, automata-theoretic methods, and abstraction."]
[null,"2.","Record Nr.",null,"UNINA9910586580503321"]
[null,null,"Autore",null,"Shoham Sharon"]
[null,null,"Titolo",null,"Computer Aided Verification : 34th International Conference, CAV 2022, Haifa, Israel, August 7–10, 2022, Proceedings, Part II / / edited by Sharon Shoham, Yakir Vizel"]
[null,null,"Pubbl/distr/stampa",null,"Cham : , : Springer International Publishing : , : Imprint : Springer, , 2022"]
[null,null,"ISBN",null,"9783031131882"]
[{"$nulls":4},"3031131886"]
[null,null,"Edizione",null,"[1st ed. 2022.]"]
[null,null,"Descrizione fisica",null,"1 online resource (560 pages) : illustrations (black and white)"]
[null,null,"Collana",null,"Lecture Notes in Computer Science, , 1611-3349 ; ; 13372"]
[null,null,"Disciplina",null,"005.1"]
[null,null,"Soggetti",null,"Software engineering"]
[{"$nulls":4},"Artificial intelligence"]
[{"$nulls":4},"Computer engineering"]
[{"$nulls":4},"Computer networks"]
[{"$nulls":4},"Computer science"]
[{"$nulls":4},"Software Engineering"]
[{"$nulls":4},"Artificial Intelligence"]
[{"$nulls":4},"Computer Engineering and Networks"]
[{"$nulls":4},"Theory of Computation"]
[null,null,"Lingua di pubblicazione",null,"Inglese"]
[null,null,"Formato",null,"Materiale a stampa"]
[null,null,null,"Livello bibliografico","Monografia"]
[null,null,"Nota di contenuto",null,"A Billion SMT Queries a Day -- Program Verification with Constrained Horn Clauses -- Formal Methods for Probabilistic Programs Data-Driven Invariant Learning for Probabilistic Programs -- Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs.-Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions -- Abstraction-Renement for Hierarchical Probabilistic Models -- Formal Methods for Neural Networks Shared Certificates for Neural Network Verification -- Example Guided Synthesis of Linear Approximations for Neural Network Verification -- Verifying Neural Networks Against Backdoor Attacks -- Trainify: A CEGAR-Driven Training and Verification Framework for Safe Deep Reinforcement Learning -- Neural Network Robustness as a Verication Property: A Principled Case Study -- Software Verication and Model Checking The Lattice-Theoretic Essence of Property Directed Reachability Analysis -- A‑ne Loop Invariant "]
[{"$nulls":4},"Generation via Matrix Algebra -- Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes -- Proof-guided Underapproximation Widening for Bounded Model Checking -- SolCMC: Solidity Compiler's Model Checker -- Sharygina Hyperproperties and Security Software Verication of Hyperproperties Beyond k-Safety -- Abstraction Modulo Stability for Reverse Engineering -- A Modular and Highly Extensible API Fuzzer for SMT Solvers -- Automata and Logic FORQ-based Language Inclusion Formal Testing -- Sound Automation of Magic Wands -- Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition -- Complementing Büchi Automata with Ranker -- Deductive Verication and Decision Procedures Even Faster Conicts and Lazier Reductions for String Solvers -- Local Search For SMT on Linear Integer Arithmetic -- Reasoning about Data Trees using CHCs -- Veried Erasure Correction in Coq with MathComp and VST -- Appel End-to-end Mechanised Proof of an eBPF Virtual Machine for Microcontrollers -- A DSL and Verication Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols -- Machine Learning Specication-Guided Learning of Nash Equilibria with High Social Welfare -- Synthesizing Fair Decision Trees via Iterative Constraint Solving -- SMT-based Translation Validation for Machine Learning Compiler -- Lee Verifying Fairness in Quantum Machine Learning -- MoGym: Using Formal Models for Training and Verifying Decision-making Agents -- Synthesis and Concurrency Synthesis and Analysis of Petri Nets from Causal Specications -- Verifying generalised and structural soundness of workow netsvia relaxations -- Capture, Analyze, Diagnose: Realizability Checking of Requirements in FRET -- Information Flow Guided Synthesis -- Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation."]
[null,null,null,"Sommario/riassunto","This open access two-volume set LNCS 13371 and 13372 constitutes the refereed proceedings of the 34rd International Conference on Computer Aided Verification, CAV 2022, which was held in Haifa, Israel, in August 2022. The 40 full papers presented together with 9 tool papers and 2 case studies were carefully reviewed and selected from 209 submissions. The papers were organized in the following topical sections: Part I: Invited papers; formal methods for probabilistic programs; formal methods for neural networks; software Verification and model checking; hyperproperties and security; formal methods for hardware, cyber-physical, and hybrid systems. Part II: Probabilistic techniques; automata and logic; deductive verification and decision procedures; machine learning; synthesis and concurrency. This is an open access book."]