Computer Aided Verification
portes grátis
Computer Aided Verification
34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part I
Shoham, Sharon; Vizel, Yakir
Springer International Publishing AG
08/2022
555
Mole
Inglês
9783031131844
15 a 20 dias
872
Descrição não disponível.
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 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 Buechi Automata based on SCC Decomposition.- Complementing Buechi 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.
Este título pertence ao(s) assunto(s) indicados(s). Para ver outros títulos clique no assunto desejado.
architecting;architecture verification and validation;artificial intelligence;computer programming;computer science;computer systems;distributed computer systems;distributed systems;embedded systems;formal logic;mathematics;model checking;programming languages;software architecture;software design;software engineering;software quality;theoretical computer science;verification;verification and validation
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 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 Buechi Automata based on SCC Decomposition.- Complementing Buechi 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.
Este título pertence ao(s) assunto(s) indicados(s). Para ver outros títulos clique no assunto desejado.
architecting;architecture verification and validation;artificial intelligence;computer programming;computer science;computer systems;distributed computer systems;distributed systems;embedded systems;formal logic;mathematics;model checking;programming languages;software architecture;software design;software engineering;software quality;theoretical computer science;verification;verification and validation
