Edizione	[1st ed. 2016.]
Pubbl/distr/stampa	Cham : , : Springer International Publishing : , : Imprint : Springer, , 2016
Descrizione fisica	1 online resource (XVII, 521 p. 126 illus.)
Disciplina	004.015113
Collana	Theoretical Computer Science and General Issues
Soggetto topico	Computer science Software engineering Machine theory Computer engineering Computer networks Computer Science Logic and Foundations of Programming Software Engineering Formal Languages and Automata Theory Computer Engineering and Networks
ISBN	3-319-41540-9
Formato	Materiale a stampa
Livello bibliografico	Monografia
Lingua di pubblicazione	eng
Nota di contenuto	Probabilistic systems -- Synthesis -- Constraint solving -- Model checking -- Program analysis -- Timed and hybrid systems -- Verification in practice -- Concurrency -- Automata and games.
Record Nr.	UNINA-9910485034903321

Edizione	[1st ed. 2015.]
Pubbl/distr/stampa	Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015
Descrizione fisica	1 online resource (XXIII, 677 p. 141 illus.)
Disciplina	004
Collana	Theoretical Computer Science and General Issues
Soggetto topico	Computer science Software engineering Machine theory Computer engineering Computer networks Computer Science Logic and Foundations of Programming Software Engineering Formal Languages and Automata Theory Computer Engineering and Networks
ISBN	3-319-21690-2
Formato	Materiale a stampa
Livello bibliografico	Monografia
Lingua di pubblicazione	eng
Nota di contenuto	A Trusted Mechanised Specification of JavaScript: One Year On -- Model Checking and Refinements -- On Automation of CTL* Verification for Infinite-State Systems -- Algorithms for Model Checking HyperLTL and HyperCTL -- Fairness Modulo Theory: A New Approach to LTL Software Model Checking -- Model Checking Parameterized Asynchronous Shared-Memory Systems -- SMT and POR Beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms -- Skipping Refinement -- Quantitative Reasoning -- Percentile Queries in Multi-dimensional Markov Decision Processes -- Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs -- Counterexample Explanation by Learning Small Strategies in Markov Decision Processes -- Symbolic Polytopes for Quantitative Interpolation and Verification -- Adaptive Aggregation of Markov Chains: Quantitative Analysis of Chemical Reaction Networks -- PROPhESY: A PRObabilistic ParamEter SYnthesis Tool -- Software Analysis -- Effective Search-Space Pruning for Solvers of String Equations, Regular Expressions and Length Constraints -- Automata-Based Model Counting for String Constraints -- OpenJDK’s Java.utils.Collection.sort() Is Broken: The Good, the Bad and the Worst Case -- Tree Buffers -- Learning Commutativity -- Specifications -- Angelic Verification: Precise Verification Modulo Unknowns -- The SeaHorn Verification Framework -- Automatic Rootcausing for Program Equivalence Failures in Binaries -- Fine-Grained Caching of Verification Results -- Predicting a Correct Program in Programming by Example -- Abstract Interpretation with Higher-Dimensional Ellipsoids and Conic Extrapolation -- Lightning Talks -- ADAM: Causality-Based Synthesis of Distributed Systems -- Alchemist: Learning Guarded Affine Functions -- OptiMathSAT: A Tool for Optimization Modulo Theories -- Systematic Asynchrony Bug Exploration for Android Apps -- Norn: An SMT Solver for String Constraints -- PVSio-web 2.0: Joining PVS to HCI -- The Hanoi Omega-Automata Format -- The Open-Source LearnLib: A Framework for Active Automata Learning -- BBS: A Phase-Bounded Model Checker for Asynchronous Programs -- Time-Aware Abstractions in HybridSal -- A Type-Directed Approach to Program Repair -- Formal Design and Safety Analysis of AIR6110 Wheel Brake System -- Meeting a Powertrain Verification Challenge -- Synthesising Executable Gene Regulatory Networks from Single-Cell Gene Expression Data -- Empirical Software Metrics for Benchmarking of Verification Tools -- Interpolation, IC3/PDR, and Invariants Property-Directed Inference of Universal Invariants or Proving Their Absence -- Efficient Anytime Techniques for Model-Based Safety Analysis -- Boosting k-induction with Continuously-Refined Invariants -- Fast Interpolating BMC -- Counterexample-Guided Polynomial Loop Invariant Generation by Lagrange Interpolation.
Record Nr.	UNISA-996204726603316

Edizione	[1st ed. 2014.]
Pubbl/distr/stampa	Cham : , : Springer International Publishing : , : Imprint : Springer, , 2014
Descrizione fisica	1 online resource (XXXIV, 877 p. 205 illus.)
Disciplina	005.1015113
Collana	Theoretical Computer Science and General Issues
Soggetto topico	Computer science Software engineering Machine theory Computer engineering Computer networks Computer Science Logic and Foundations of Programming Software Engineering Formal Languages and Automata Theory Computer Engineering and Networks
ISBN	3-319-08867-X
Formato	Materiale a stampa
Livello bibliografico	Monografia
Lingua di pubblicazione	eng
Nota di contenuto	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 Simple and 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.
Record Nr.	UNISA-996199992703316

Edizione	[1st ed. 2013.]
Pubbl/distr/stampa	Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2013
Descrizione fisica	1 online resource (XXII, 1015 p. 237 illus.)
Disciplina	005.14
Collana	Theoretical Computer Science and General Issues
Soggetto topico	Computer science Software engineering Computers, Special purpose Computer Science Logic and Foundations of Programming Software Engineering Special Purpose and Application-Based Systems
ISBN	3-642-39799-9
Formato	Materiale a stampa
Livello bibliografico	Monografia
Lingua di pubblicazione	eng
Nota di contenuto	Automata Networks -- Model-Checking Signal Transduction Networks through Decreasing Reachability Sets -- TTP: Tool for Tumor Progression -- Exploring Parameter Space of Stochastic Biochemical Systems using Quantitative Model Checking -- Parameterized Verification of Asynchronous Shared-Memory Systems -- Partial Orders for Efficient BMC of Concurrent Software -- Incremental, Inductive Coverability -- Automatic linearizability proofs of concurrent objects with cooperating -- Updates -- Duet: Static Analysis for Unbounded Parallelism -- SVA and PSL Local Variables -- A Practical Approach -- Formal Verification of Hardware Synthesis -- CacBDD: A BDD Package with Dynamic Cache Management -- Distributed Explicit State Model Checking of Deadlock Freedom -- Exponential-Condition-Based Barrier Certificate Generation for Safety -- Verification of Hybrid Systems -- Efficient Robust Monitoring for STL -- Abstraction based Model-Checking of Stability of Hybrid Systems -- Faster Algorithms for Markov Decision Processes with Low Tree width -- Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis -- Importance Splitting for Statistical Model Checking Rare Properties -- Minimal Sets over Monotone Predicates in Boolean Formulae -- Smten: Automatic Translation of High-level Symbolic Computations into SMT Queries -- QUAIL: a quantitative security analyzer for imperative code -- Effectively Propositional Reasoning about Reachability in Linked Data Structures -- Learning Universally Quantified Invariants of Linear Data Structures -- GOAL for Games, Omega-Automata, and Logics -- Efficient synthesis for concurrency using semantics-preserving Transformations.
Record Nr.	UNISA-996466042903316

Edizione	[1st ed. 2012.]
Pubbl/distr/stampa	Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2012
Descrizione fisica	1 online resource (XVI, 789 p. 192 illus.)
Disciplina	005.1015113
Collana	Theoretical Computer Science and General Issues
Soggetto topico	Computer science Software engineering Machine theory Artificial intelligence Computers, Special purpose Computers Computer Science Logic and Foundations of Programming Software Engineering Formal Languages and Automata Theory Artificial Intelligence Special Purpose and Application-Based Systems Computer Hardware
ISBN	3-642-31424-4
Formato	Materiale a stampa
Livello bibliografico	Monografia
Lingua di pubblicazione	eng
Record Nr.	UNISA-996465526003316