26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014, Proceedings Redaktion: Biere, Armin; Bloem, Roderick
26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014, Proceedings Redaktion: Biere, Armin; Bloem, Roderick
Sie sind bereits eingeloggt. Klicken Sie auf 2. tolino select Abo, um fortzufahren.
Bitte loggen Sie sich zunächst in Ihr Kundenkonto ein oder registrieren Sie sich bei bücher.de, um das eBook-Abo tolino select nutzen zu können.
This book constitutes the proceedings of the 26th International Conference on Computer Aided Verification, CAV 2014, held as part of the Vienna Summer of Logic, VSL 2014, in Vienna, Austria, in July 2014. The 46 regular papers and 11 short papers presented in this volume were carefully reviewed and selected from a total of 175 regular and 54 short paper submissions. The contributions are organized in topical sections named: software verification; automata; model checking and testing; biology and hybrid systems; games and synthesis; concurrency; SMT and theorem proving; bounds and termination; and abstraction.…mehr
This book constitutes the proceedings of the 26th International Conference on Computer Aided Verification, CAV 2014, held as part of the Vienna Summer of Logic, VSL 2014, in Vienna, Austria, in July 2014. The 46 regular papers and 11 short papers presented in this volume were carefully reviewed and selected from a total of 175 regular and 54 short paper submissions. The contributions are organized in topical sections named: software verification; automata; model checking and testing; biology and hybrid systems; games and synthesis; concurrency; SMT and theorem proving; bounds and termination; and abstraction.
Dieser Download kann aus rechtlichen Gründen nur mit Rechnungsadresse in A, B, BG, CY, CZ, D, DK, EW, E, FIN, F, GR, HR, H, IRL, I, LT, L, LR, M, NL, PL, P, R, S, SLO, SK ausgeliefert werden.
Die Herstellerinformationen sind derzeit nicht verfügbar.
Inhaltsangabe
Software Verification.- The Spirit of Ghost Code.- SMT-Based Model Checking for Recursive Programs.- Property-Directed Shape Analysis.- Shape Analysis via Second-Order Bi-Abduction.- ICE: A Robust Framework for Learning Invariants.- From Invariant Checking to Invariant Inference Using Randomized Search.- SMACK: Decoupling Source Language Details from Verifier Implementations.- Security.- Synthesis of Masking Countermeasures against Side Channel Attacks.- Temporal Mode-Checking for Runtime Monitoring of Privacy Policies.- String Constraints for Verification.- A Conference Management System with Verified Document Confidentiality.- VAC - Verifier of Administrative Role-Based Access Control Policies.- Automata.- From LTL to Deterministic Automata: A Safraless Compositional Approach.- Symbolic Visibly Pushdown Automata.- Model Checking and Testing.- Engineering a Static Verification Tool for GPU Kernels.- Lazy Annotation Revisited.- Interpolating Property Directed Reachability.- Verifying Relative Error Bounds Using Symbolic Simulation.- Regression Test Selection for Distributed Software Histories.- GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components.- Software Verification in the Google App-Engine Cloud.- The nuXmv Symbolic Model Checker.- Biology and Hybrid Systems Analyzing and Synthesizing Genomic Logic Functions.- Finding Instability in Biological Models.- Invariant Verification of Nonlinear Hybrid Automata Networks of Cardiac Cells.- Diamonds Are a Girl's Best Friend: Partial Order Reduction for Timed Automata with Abstractions.- Reachability Analysis of Hybrid Systems Using Symbolic Orthogonal Projections.- Verifying LTL Properties of Hybrid Systems with K-Liveness.- Games and Synthesis.- Safraless Synthesis for Epistemic Temporal Specifications.- Minimizing Running Costs in Consumption Systems.- CEGAR for Qualitative Analysis of Probabilistic Systems.- Optimal Guard Synthesis for Memory Safety.- Don't Sit on the Fence: A Static Analysis Approach to Automatic Fence Insertion.- MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications.- Solving Games without Controllable Predecessor.- G4LTL-ST: Automatic Generation of PLC Programs.- Concurrency.- Automatic Atomicity Verification for Clients of Concurrent Data Structures.- Regression-Free Synthesis for Concurrency.- Bounded Model Checking of Multi-threaded C Programs via Lazy Sequentialization.- An SMT-Based Approach to Coverability Analysis.- LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes.- SMT and Theorem Proving.- Monadic Decomposition.- A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions.- Bit-Vector Rewriting with Automatic Rule Generation.- A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors.- AVATAR: The Architecture for First-Order Theorem Provers.- Automating Separation Logic with Trees and Data.- A Nonlinear Real Arithmetic Fragment.- Yices 2.2.- Bounds and Termination.- A Simpleand Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis.- Symbolic Resource Bound Inference for Functional Programs.- Proving Non-termination Using Max-SMT.- Termination Analysis by Learning Terminating Programs.- Causal Termination of Multi-threaded Programs.- Abstraction.- Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR).- Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction.- QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers.
Software Verification.- The Spirit of Ghost Code.- SMT-Based Model Checking for Recursive Programs.- Property-Directed Shape Analysis.- Shape Analysis via Second-Order Bi-Abduction.- ICE: A Robust Framework for Learning Invariants.- From Invariant Checking to Invariant Inference Using Randomized Search.- SMACK: Decoupling Source Language Details from Verifier Implementations.- Security.- Synthesis of Masking Countermeasures against Side Channel Attacks.- Temporal Mode-Checking for Runtime Monitoring of Privacy Policies.- String Constraints for Verification.- A Conference Management System with Verified Document Confidentiality.- VAC - Verifier of Administrative Role-Based Access Control Policies.- Automata.- From LTL to Deterministic Automata: A Safraless Compositional Approach.- Symbolic Visibly Pushdown Automata.- Model Checking and Testing.- Engineering a Static Verification Tool for GPU Kernels.- Lazy Annotation Revisited.- Interpolating Property Directed Reachability.- Verifying Relative Error Bounds Using Symbolic Simulation.- Regression Test Selection for Distributed Software Histories.- GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components.- Software Verification in the Google App-Engine Cloud.- The nuXmv Symbolic Model Checker.- Biology and Hybrid Systems Analyzing and Synthesizing Genomic Logic Functions.- Finding Instability in Biological Models.- Invariant Verification of Nonlinear Hybrid Automata Networks of Cardiac Cells.- Diamonds Are a Girl's Best Friend: Partial Order Reduction for Timed Automata with Abstractions.- Reachability Analysis of Hybrid Systems Using Symbolic Orthogonal Projections.- Verifying LTL Properties of Hybrid Systems with K-Liveness.- Games and Synthesis.- Safraless Synthesis for Epistemic Temporal Specifications.- Minimizing Running Costs in Consumption Systems.- CEGAR for Qualitative Analysis of Probabilistic Systems.- Optimal Guard Synthesis for Memory Safety.- Don't Sit on the Fence: A Static Analysis Approach to Automatic Fence Insertion.- MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications.- Solving Games without Controllable Predecessor.- G4LTL-ST: Automatic Generation of PLC Programs.- Concurrency.- Automatic Atomicity Verification for Clients of Concurrent Data Structures.- Regression-Free Synthesis for Concurrency.- Bounded Model Checking of Multi-threaded C Programs via Lazy Sequentialization.- An SMT-Based Approach to Coverability Analysis.- LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes.- SMT and Theorem Proving.- Monadic Decomposition.- A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions.- Bit-Vector Rewriting with Automatic Rule Generation.- A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors.- AVATAR: The Architecture for First-Order Theorem Provers.- Automating Separation Logic with Trees and Data.- A Nonlinear Real Arithmetic Fragment.- Yices 2.2.- Bounds and Termination.- A Simpleand Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis.- Symbolic Resource Bound Inference for Functional Programs.- Proving Non-termination Using Max-SMT.- Termination Analysis by Learning Terminating Programs.- Causal Termination of Multi-threaded Programs.- Abstraction.- Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR).- Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction.- QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers.
Es gelten unsere Allgemeinen Geschäftsbedingungen: www.buecher.de/agb
Impressum
www.buecher.de ist ein Internetauftritt der buecher.de internetstores GmbH
Geschäftsführung: Monica Sawhney | Roland Kölbl | Günter Hilger
Sitz der Gesellschaft: Batheyer Straße 115 - 117, 58099 Hagen
Postanschrift: Bürgermeister-Wegele-Str. 12, 86167 Augsburg
Amtsgericht Hagen HRB 13257
Steuernummer: 321/5800/1497
USt-IdNr: DE450055826
