Info
- Utilizzare la checkbox di selezione a fianco di ciascun documento per attivare le funzionalità di stampa, invio email, download nei formati disponibili del (i) record.
Automated Technology for Verification and Analysis : 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings / / edited by Cyrille Artho, Axel Legay, Doron Peled
| Automated Technology for Verification and Analysis : 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings / / edited by Cyrille Artho, Axel Legay, Doron Peled |
| Edizione | [1st ed. 2016.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2016 |
| Descrizione fisica | 1 online resource (XI, 530 p. 102 illus.) |
| Disciplina | 004.015113 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Software engineering
Compilers (Computer programs) Computer science Machine theory Artificial intelligence Computer programming Software Engineering Compilers and Interpreters Computer Science Logic and Foundations of Programming Formal Languages and Automata Theory Artificial Intelligence Programming Techniques |
| ISBN | 3-319-46520-1 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Keynote -- Synthesizing and Completely Testing Hardware based on Templates through Small Numbers of Test Patterns -- Markov Models, Chains, and Decision Processes -- Approximate Policy Iteration for Markov Decision Processes via Quantitative Adaptive Aggregations. -Optimizing the Expected Mean Payoff in Energy Markov Decision Processes -- Parameter Synthesis for Markov Models: Faster Than Ever -- Bounded Model Checking for Probabilistic Programs -- Counter Systems, Automata -- How Hard Is It to Verify Flat Affine Counter Systems with the Finite Monoid Property -- Solving Language Equations using Flanked Automata -- Spot 2.0 - a Framework for LTL and ω-Automata Manipulation -- MoChiBA: Probabilistic LTL Model Checking Using Limit- Deterministic Büchi Automata -- Parallelism, Concurrency -- Synchronous Products of Rewrite Systems -- Specifying and Verifying Secrecy in Workflows with Arbitrarily Many Agents -- Lazy Sequentialization for the Safety Verification of Unbounded Concurrent Programs -- Parallel SMT-Based Parameter Synthesis with Application to Piecewise Multi-Affine Systems -- Complexity, Decidability -- On Finite Domains in First-Order Linear Temporal Logic -- Decidability Results for Multi-Objective Stochastic Games -- A Decision Procedure for Separation Logic in SMT -- Solving Mean-Payoff Games on the GPU -- Synthesis, Refinement -- Synthesizing Skeletons for Reactive Systems -- Observational Refinement and Merge for Disjunctive MTSs -- Equivalence-Based Abstraction Refinement for muHORS Model Checking -- Optimization, Heuristics, Partial-Order Reductions -- Greener Bits: Formal Analysis of Demand Response -- Heuristics for Checking Liveness Properties with Partial Order Reductions. - Partial-Order Reduction for GPU Model Checking -- Efficient Verification of Program Fragments: Eager POR -- Solving Procedures, Model Checking -- Skolem Functions for DQBF -- STL Model Checking of Continuous and Hybrid Systems -- Clause Sharing and Partitioning for Cloud-Based SMT Solving -- Symbolic Model Checking for Factored Probabilistic Models -- Program Analysis -- A Sketching-Based Approach for Debugging Using Test Cases -- Polynomial Invariants by Linear Algebra -- Certified Symbolic Execution -- Tighter Loop Bound Analysis. . |
| Record Nr. | UNINA-9910483188903321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2016 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Automated Technology for Verification and Analysis : 13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015, Proceedings / / edited by Bernd Finkbeiner, Geguang Pu, Lijun Zhang
| Automated Technology for Verification and Analysis : 13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015, Proceedings / / edited by Bernd Finkbeiner, Geguang Pu, Lijun Zhang |
| Edizione | [1st ed. 2015.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 |
| Descrizione fisica | 1 online resource (XIII, 520 p. 96 illus.) |
| Disciplina | 005.13 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Compilers (Computer programs)
Computer science Machine theory Artificial intelligence Computer programming Compilers and Interpreters Computer Science Logic and Foundations of Programming Formal Languages and Automata Theory Artificial Intelligence Programming Techniques |
| ISBN | 3-319-24953-3 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Preface -- Organization -- Contents -- Probabilistic Programming: A True Verification Challenge -- References -- Machines Reasoning About Machines: 2015 -- 1 Introduction -- 2 A Quick History and Acknowledgments -- 3 1970s -- Simple List Processing -- 4 1980s -- Academic Math and Computer Science -- 5 1990s -- Commercial Breakthrough -- 6 2000s -- Gradual Acceptance -- 7 2010 -- Integrated with the Design Process -- 8 Lessons -- 9 Conclusion -- References -- Using SMT for Solving Fragments of Parameterised Boolean Equation Systems -- 1 Introduction -- 2 Preliminaries -- 3 A Motivating Example -- 4 Disjunctive and Conjunctive PBESs -- 5 Solving Disjunctive and Conjunctive PBESs Using SMT -- 5.1 Finding Lasso-Shaped Proof Graphs -- 5.2 Proving the Absence of Proof Graphs -- 5.3 A Pseudo-Decision Procedure -- 6 Experiments -- 7 Closing Remarks -- References -- Unfolding-Based Process Discovery -- 1 Introduction -- 2 Preliminaries -- 3 Independence-Preserving Discovery -- 4 Introducing Generalization -- 4.1 Language-Preserving Generalization -- 4.2 Controlling Generalization via Negative Information -- 5 Computing Folding Equivalences -- 5.1 SMT Encoding -- 5.2 Finding an Optimal Folding Equivalence -- 6 Experiments -- 7 Related Work -- 8 Conclusions -- References -- Improving Interpolants for Linear Arithmetic -- 1 Introduction -- 2 Preliminaries -- 2.1 Notations -- 2.2 Computing Interpolants by Resolution Proofs -- 2.3 Computing Interpolants by DC-Removability Checks -- 2.4 Description of a State Set -- 3 The General Algorithm -- 3.1 Test Whether One Additional Linear Constraint Is Sufficient -- 3.2 Finding Pairs of Indistinguishable Points with SMT -- 3.3 Enlarge Pairs of Indistinguishable Points to Convex Regions -- 3.4 Finding a Linear Constraint Separating Pairs of Convex Regions with LP -- 4 Optimizations -- 5 Experimental Results.
6 Conclusion and Further Research -- References -- A Mechanically Checked Generation of Correlating Programs Directed by Structured Syntactic Differences -- 1 Introduction -- 2 Overview -- 3 Source Language and Its Guarded Form -- 3.1 Input Language -- 3.2 Guarded Language -- 3.3 Translation to Guarded Form -- 4 Structured Differences Between Programs -- 5 Generation Algorithm Directed by Structured Differences -- 6 Implementation and Experiments -- 7 Related Work -- 8 Conclusion -- References -- On Automated Lemma Generation for Separation Logic with Inductive Definitions -- 1 Introduction -- 2 Motivating Example -- 3 Separation Logic with Inductive Definitions -- 4 Composition Lemmas -- 5 Derived Lemmas -- 5.1 The ``Completion'' Lemmas -- 5.2 The ``Stronger'' Lemmas -- 6 A Proof Strategy Based on Lemmas -- 7 Experimental Results -- 8 Related Work -- 9 Conclusion -- References -- Severity Levels of Inconsistent Code -- 1 Introduction -- 2 Overview -- 3 Inconsistent Code -- 4 Severity Levels of Inconsistency -- 5 Algorithm for Categorizing Inconsistent Code -- 6 Evaluation -- 7 Related Work -- 8 Conclusion -- References -- Learning the Language of Error -- 1 Introduction -- 2 Preliminaries -- the L* Algorithm -- 3 The Language We Learn -- 4 L* and the Queries -- 4.1 Membership Queries -- 4.2 Conjecture Queries -- 5 Usage Scenarios for the Learning Framework -- 6 System Description and Empirical Evaluation -- 6.1 Optimisations -- 6.2 Implementation and Evaluation -- 7 Conclusions and Future Work -- References -- Explicit Model Checking of Very Large MDP Using Partitioning and Secondary Storage -- 1 Introduction -- 2 Preliminaries -- 3 Disk-Based State Space Exploration with Partitioning -- 3.1 Representation of MDP in Memory and on Disk -- 3.2 Disk-Based Exploration Using Partitioning -- 4 Disk-Based Partitioned Value Iteration -- 5 Evaluation. 6 Conclusion -- References -- Model Checking Failure-Prone Open Systems Using Probabilistic Automata -- 1 Introduction -- 2 Preliminaries -- 2.1 Hierarchical Probabilistic Automata -- 3 Decision Algorithms and Robustness -- 3.1 Forward Algorithm -- 3.2 Backward Algorithm -- 3.3 Forward vs. Backward -- 3.4 Robustness -- 4 Undecidability for 2-HPA -- 5 Modeling Failure-Prone Open Systems -- 6 Implementation and Experiment -- 6.1 Implementation of the Verification Algorithms -- 6.2 Abstracting Models of Web Applications -- 6.3 Experiment -- 7 Conclusions -- References -- Optimal Continuous Time Markov Decisions -- 1 Introduction -- 2 Preliminaries -- 3 Unif+: Optimal Time-Bounded Reachability Revisited -- 3.1 Uniformisation to C -- 3.2 Lower and Upper Bounds on the Value of C -- 3.3 Convergence of the Bounds for Increasing -- 3.4 Extracting the Scheduler -- 4 Existing Algorithms -- 5 Empirical Evaluation and Comparison -- 6 Conclusion -- References -- Spanning the Spectrum from Safety to Liveness -- 1 Introduction -- 2 Preliminaries -- 3 Classes of Safety -- 3.1 Co-safety -- 3.2 Finding the Safety Level -- 4 Finding the Safety Class -- 4.1 Observations on Automata -- 4.2 Expressive Power -- 4.3 Decision Procedures -- 5 Discussion and Directions for Future Research -- References -- Marimba: A Tool for Verifying Properties of Hidden Markov Models -- 1 Introduction -- 2 Tool Architecture and Implementation -- 2.1 Marimba's Input and Modules -- 3 Verification of a Human-Robot Interaction -- 4 Conclusions -- References -- ParaVerifier: An Automatic Framework for Proving Parameterized Cache Coherence Protocols -- 1 Introduction -- 2 Consistency Lemma -- 3 Overview of Our Approach -- 4 Validation and Conclusion -- References -- ASSA-PBN: An Approximate Steady-State Analyser of Probabilistic Boolean Networks -- 1 Introduction -- 2 Architecture and Usage. 3 Comparison, Evaluation and Future Developments -- References -- EviCheck: Digital Evidence for Android -- 1 Introduction and Related Work -- 2 EviCheck's Main Ingredients -- 2.1 Policy Language -- 2.2 The Verifier -- 2.3 The Checker -- 2.4 Policy Generator -- 2.5 Technical Discussion -- 3 Implementation and Experiments -- References -- Lazy-CSeq-SP: Boosting Sequentialization-Based Verification of Multi-threaded C Programs via Symbolic Pruning of Redundant Schedules -- 1 Introduction -- 2 Optimized Scheduler Encoding -- 3 Implementation Details -- 4 Experimental Evaluation and Conclusion -- References -- A Contextual Equivalence Checker for IMJ* -- 1 Introduction -- 2 Tool Architecture -- 3 Evaluation -- References -- Trace Diagnostics Using Temporal Implicants -- 1 Introduction -- 2 Propositional Foundations -- 2.1 Problem Statement -- 2.2 Syntactic and Semantic Formulations -- 2.3 Practical Solution -- 3 Temporal Issues -- 3.1 Syntactic Rewritings -- 3.2 Semantic Restrictions -- 3.3 Sub-models of a Formula -- 3.4 Temporal Implicants -- 4 MTL Diagnostics -- 4.1 Non-Standard MTL Semantics -- 4.2 Explanation Operators -- 4.3 Computation of Selection Functions -- 4.4 Discussion -- 5 LTL Ultimately-Periodic Diagnostics -- 5.1 Recurrent LTL Semantics -- 5.2 Explanation Operators -- 6 Conclusion and Perspectives -- References -- Test Case Generation of Actor Systems -- 1 Introduction -- 2 The Language -- 3 Symbolic Execution -- 4 Less Redundant Exploration in Symbolic Execution -- 5 Generation of Test Cases -- 5.1 Coverage and Termination Criteria for Actor Systems -- 5.2 Test Cases for Actor Systems -- 6 Implementation and Experimental Evaluation -- 7 Related Work and Conclusions -- References -- Lattice-Based Semantics for Combinatorial Model Evolution -- 1 Introduction -- 2 Running Example and Overview -- 3 Preliminaries. 4 Lattice-Based Semantics for Combinatorial Model Evolution -- 5 Atomic Operations on Combinatorial Models -- 5.1 Adding or Removing a Parameter and Its Values -- 5.2 Adding or Removing a Value from an Existing Parameter -- 5.3 Adding, Removing, or Changing a Constraint -- 6 Split and Merge Operations on Combinatorial Models -- 7 Related Work -- 8 Summary and Future Work -- References -- Effective Verification of Replicated Data Types Using Later Appearance Records (LAR) -- 1 Introduction -- 2 CRDTs, Traces and Specifications -- 3 CRDT Implementation -- 3.1 Reference Implementation -- 3.2 Details of the Reference Implementation -- 3.3 Correctness of the Reference Implementation -- 3.4 Bounding the Reference Implementation -- 4 Effective Verification Using Bounded Reference Implementation via CEGAR -- 5 Conclusion -- References -- TSO-to-TSO Linearizability Is Undecidable -- 1 Introduction -- 2 TSO Concurrent Systems -- 2.1 Notations -- 2.2 Libraries and the Most General Clients -- 2.3 TSO Operational Semantics -- 3 TSO-to-TSO Linearizability and Equivalent Characterization -- 3.1 TSO-to-TSO Linearizability -- 3.2 Equivalence Characterization -- 4 Undecidability of TSO-to-TSO Linearizability -- 4.1 Classic-Lossy Single-Channel Systems -- 4.2 Simulation on the TSO Memory Model -- 4.3 Undecidability of History Inclusion -- 4.4 Undecidability of TSO-to-TSO Linearizability -- 5 Conclusion and Future Work -- References -- Formal Verification of Infinite-State BIP Models -- 1 Introduction -- 2 The BIP Model -- 3 ESST for BIP (ESST BIP ) -- 3.1 The ESST Framework -- 3.2 Instantiation of ESST for BIP -- 3.3 Optimizations -- 4 Encoding BIP into Transition System -- 5 Related Work -- 6 Experimental Evaluation -- 7 Conclusions and Future Work -- References -- PBMC: Symbolic Slicing for the Verification of Concurrent Programs -- 1 Introduction. 2 Motivating Example. |
| Record Nr. | UNINA-9910484603403321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Automated Technology for Verification and Analysis : 12th International Symposium, ATVA 2014, Sydney, Australia, November 3-7, 2014, Proceedings / / edited by Franck Cassez, Jean-Francois Raskin
| Automated Technology for Verification and Analysis : 12th International Symposium, ATVA 2014, Sydney, Australia, November 3-7, 2014, Proceedings / / edited by Franck Cassez, Jean-Francois Raskin |
| Edizione | [1st ed. 2014.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2014 |
| Descrizione fisica | 1 online resource (XXIV, 430 p. 109 illus.) |
| Disciplina | 004 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Software engineering
Computer programming Computer networks Computer science Compilers (Computer programs) Machine theory Software Engineering Programming Techniques Computer Communication Networks Computer Science Logic and Foundations of Programming Compilers and Interpreters Formal Languages and Automata Theory |
| ISBN | 3-319-11936-2 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Verifying Communicating Multi-pushdown Systems via Split-Width -- Booster: An Acceleration-Based Verification Framework for Array Programs -- A Bounded Model Checker for SPARK Programs -- Acceleration of Affine Hybrid Transformations -- A Mechanized Proof of Loop Freedom of the (Untimed) AODV Routing Protocol -- Quantitative Verification of Weighted Kripke Structures -- Formal Safety Assessment via Contract-Based Design -- Verification of Markov Decision Processes Using Learning Algorithms -- Test Coverage Estimation Using Threshold Accepting -- On Time with Minimal Expected Cost! -- Fast Debugging of PRISM Models -- ACME: Automata with Counters, Monoids and Equivalence (Tool Paper).-Modelling and Analysis of Markov Reward Automata -- Extensional Crisis and Proving Identity -- Deciding Entailments in Inductive Separation Logic with Tree Automata -- Liveness Analysis for Parameterised Boolean Equation Systems -- Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata -- PeCAn: Compositional Verification of Petri Nets Made Easy -- The Context-Freeness Problem Is coNP-Complete for Flat Counter Systems -- Efficiently and Completely Verifying Synchronized Consistency Models -- Symmetry Reduction in Infinite Games with Finite Branching -- Incremental Encoding and Solving of Cardinality Constraints -- Formal Verification of Skiplists with Arbitrary Many Levels -- Using Flow Specifications of Parameterized Cache Coherence Protocols for Verifying Deadlock Freedom -- A Game-Theoretic Approach to Simulation of Data-Parameterized Systems -- Nested Reachability Approximation for Discrete-Time Markov Chains with Univariate Parameters -- Symbolic Memory with Pointers -- Trace Abstraction Refinement for Timed Automata -- Statistically Sound Verification and Optimization for Complex Systems. |
| Record Nr. | UNINA-9910484040303321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2014 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Automated Technology for Verification and Analysis : 11th International Symposium, ATVA 2013, Hanoi, Vietnam, October 15-18, 2013, Proceedings / / edited by Dang Van Hung, Mizuhito Ogawa
| Automated Technology for Verification and Analysis : 11th International Symposium, ATVA 2013, Hanoi, Vietnam, October 15-18, 2013, Proceedings / / edited by Dang Van Hung, Mizuhito Ogawa |
| Edizione | [1st ed. 2013.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2013 |
| Descrizione fisica | 1 online resource (XIV, 528 p. 115 illus.) |
| Disciplina | 004.015113 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Software engineering
Computer programming Computer networks Computer science Compilers (Computer programs) Software Engineering Programming Techniques Computer Communication Networks Computer Science Logic and Foundations of Programming Compilers and Interpreters |
| ISBN | 3-319-02444-2 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Papers.-Acceleration for Petri Nets -- Automated Verification and Strategy Synthesis for Probabilistic Systems -- SMT-Based Software Model Checking: Explicit Scheduler, Symbolic Threads -- Regular Papers.-Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F,G)-Fragment -- Improved Upper and Lower Bounds for B¨uchi Disambiguation -- Time-Bounded Reachability for Monotonic Hybrid Automata: Complexity and Fixed Points -- An Automatic Technique for Checking the Simulation of Timed Systems -- Synthesis of Bounded Integer Parameters for Parametric Timed Reachability Games -- Kleene Algebras and Semimodules for Energy Problems -- Looking at Mean-Payoff and Total-Payoff through Windows -- Weighted Safety -- A Framework for Ranking Vacuity Results -- Synthesizing Masking Fault-Tolerant Systems from Deontic Specifications -- Verification of a Dynamic Management Protocol for Cloud Applications -- Compact Symbolic Execution -- Multi-threaded Explicit State Space Exploration with State Reconstruction -- Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata -- Integrating Policy Iterations in Abstract Interpreters -- Interpolation Properties and SAT-Based Model Checking -- Analysis of Message Passing Programs Using SMT-Solvers -- An Expressive Framework for Verifying Deadlock Freedom -- Expected Termination Time in BPA Games -- Precise Cost Analysis via Local Reasoning -- Control Flow Refinement and Symbolic Computation of Average Case Bound -- Termination and Cost Analysis of Loops with Concurrent Interleavings -- Linear Ranking for Linear Lasso Programs -- Merge and Conquer: State Merging in Parametric Timed Automata -- An Automata-Theoretic Approach to Reasoning about Parameterized Systems and Specifications -- Pushdown Systems with Stack Manipulation -- Robustness Analysis of String Transducers -- Tool Papers -- Manipulating LTL Formulas Using Spot 1.0 -- Rabinizer 2: Small Deterministic Automata for LTL\GU -- LTL Model Checking with Neco.-Solving Parity Games on the GPU -- PyEcdar: Towards Open Source Implementation for Timed Systems -- CCMC: A Conditional CSL Model Checker for Continuous-Time Markov Chains -- NLTOOLBOX: A Library for Reachability Computation of Nonlinear Dynamical Systems -- CELL: A Compositional Verification Framework -- VCS: A Verifier for Component-Based Systems -- SmacC: A Retargetable Symbolic Execution Engine -- MoTraS: A Tool for Modal Transition Systems and Their Extensions -- Cunf: A Tool for Unfolding and Verifying Petri Nets with Read Arcs -- Short Papers -- SAT Based Verification of Network Data Planes -- A Theory for Control-Flow Graph Exploration -- The Quest for Precision: A Layered Approach for Data Race Detection in Static Analysis. |
| Record Nr. | UNINA-9910484686403321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2013 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Automated Technology for Verification and Analysis : 8th International Symposium, ATVA 2010, Singapore, September 21-24, 2010, Proceedings / / edited by Ahmed Bouajjani, Wei-Ngan Chin
| Automated Technology for Verification and Analysis : 8th International Symposium, ATVA 2010, Singapore, September 21-24, 2010, Proceedings / / edited by Ahmed Bouajjani, Wei-Ngan Chin |
| Edizione | [1st ed. 2010.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2010 |
| Descrizione fisica | 1 online resource (VIII, 404 p. 112 illus.) |
| Disciplina | 511.3/6028563 |
| Altri autori (Persone) |
BouajjaniAhmed
ChinWei-Ngan |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Software engineering
Computer programming Computer networks Computer science Compilers (Computer programs) Software Engineering Programming Techniques Computer Communication Networks Computer Science Logic and Foundations of Programming Compilers and Interpreters |
| ISBN |
1-280-38884-6
9786613566768 3-642-15643-6 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- Probabilistic Automata on Infinite Words: Decidability and Undecidability Results -- Abstraction Learning -- Synthesis: Words and Traces -- Regular Papers -- Promptness in ?-Regular Automata -- Using Redundant Constraints for Refinement -- Methods for Knowledge Based Controlling of Distributed Systems -- Composing Reachability Analyses of Hybrid Systems for Safety and Stability -- The Complexity of Codiagnosability for Discrete Event and Timed Systems -- On Scenario Synchronization -- Compositional Algorithms for LTL Synthesis -- What’s Decidable about Sequences? -- A Study of the Convergence of Steady State Probabilities in a Closed Fork-Join Network -- Lattice-Valued Binary Decision Diagrams -- A Specification Logic for Exceptions and Beyond -- Non-monotonic Refinement of Control Abstraction for Concurrent Programs -- An Approach for Class Testing from Class Contracts -- Efficient On-the-Fly Emptiness Check for Timed Büchi Automata -- Reachability as Derivability, Finite Countermodels and Verification -- LTL Can Be More Succinct -- Automatic Generation of History-Based Access Control from Information Flow Specification -- Auxiliary Constructs for Proving Liveness in Compassion Discrete Systems -- Symbolic Unfolding of Parametric Stopwatch Petri Nets -- Recursive Timed Automata -- Probabilistic Contracts for Component-Based Design -- Tool Papers -- Model-Checking Web Applications with Web-TLR -- GAVS: Game Arena Visualization and Synthesis -- CRI: Symbolic Debugger for MCAPI Applications -- MCGP: A Software Synthesis Tool Based on Model Checking and Genetic Programming -- ECDAR: An Environment for Compositional Design and Analysis of Real Time Systems -- Developing Model Checkers Using PAT -- YAGA: Automated Analysis of Quantitative Safety Specifications in Probabilistic B.-COMBINE: A Tool on Combined Formal Methods for Bindingly Verification -- Rbminer: A Tool for Discovering Petri Nets from Transition Systems. |
| Record Nr. | UNINA-9910485034203321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2010 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Automated Technology for Verification and Analysis : 7th International Symposium, ATVA 2009, Macao, China, October 14-16, 2009, Proceedings / / edited by Zhiming Liu, Anders P. Ravn
| Automated Technology for Verification and Analysis : 7th International Symposium, ATVA 2009, Macao, China, October 14-16, 2009, Proceedings / / edited by Zhiming Liu, Anders P. Ravn |
| Edizione | [1st ed. 2009.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009 |
| Descrizione fisica | 1 online resource (XI, 414 p.) |
| Disciplina | 004n/a |
| Altri autori (Persone) |
LiuZhiming <1961->
RavnAnders P |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Computer science
Computer programming Compilers (Computer programs) Machine theory Algorithms Theory of Computation Programming Techniques Compilers and Interpreters Computer Science Logic and Foundations of Programming Formal Languages and Automata Theory |
| ISBN | 3-642-04761-0 |
| Classificazione |
DAT 286f
DAT 325f DAT 704f SS 4800 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- Verifying VLSI Circuits -- 3-Valued Abstraction for (Bounded) Model Checking -- Local Search in Model Checking -- State Space Reduction -- Exploring the Scope for Partial Order Reduction -- State Space Reduction of Linear Processes Using Control Flow Reconstruction -- A Data Symmetry Reduction Technique for Temporal-epistemic Logic -- Tools -- TAPAAL: Editor, Simulator and Verifier of Timed-Arc Petri Nets -- CLAN: A Tool for Contract Analysis and Conflict Discovery -- UnitCheck: Unit Testing and Model Checking Combined -- Probabilistic Systems -- LTL Model Checking of Time-Inhomogeneous Markov Chains -- Statistical Model Checking Using Perfect Simulation -- Quantitative Analysis under Fairness Constraints -- A Decompositional Proof Scheme for Automated Convergence Proofs of Stochastic Hybrid Systems -- Medley -- Memory Usage Verification Using Hip/Sleek -- Solving Parity Games in Practice -- Automated Analysis of Data-Dependent Programs with Dynamic Memory -- Temporal Logic I -- On-the-fly Emptiness Check of Transition-Based Streett Automata -- On Minimal Odd Rankings for Büchi Complementation -- Specification Languages for Stutter-Invariant Regular Properties -- Abstraction and Refinement -- Incremental False Path Elimination for Static Software Analysis -- A Framework for Compositional Verification of Multi-valued Systems via Abstraction-Refinement -- Don’t Know for Multi-valued Systems -- Logahedra: A New Weakly Relational Domain -- Fault Tolerant Systems -- Synthesis of Fault-Tolerant Distributed Systems -- Formal Verification for High-Assurance Behavioral Synthesis -- Dynamic Observers for the Synthesis of Opaque Systems -- Temporal Logic II -- Symbolic CTL Model Checking of Asynchronous Systems Using Constrained Saturation -- LTL Model Checking for Recursive Programs -- OnDetecting Regular Predicates in Distributed Systems. |
| Record Nr. | UNINA-9910484140503321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Automated Technology for Verification and Analysis : 6th International Symposium, ATVA 2008, Seoul, Korea, October 20-23, 2008, Proceedings / / edited by Sungdeok Cha, Jin-Young Choi, Moonzoo Kim, Mahesh Viswanathan
| Automated Technology for Verification and Analysis : 6th International Symposium, ATVA 2008, Seoul, Korea, October 20-23, 2008, Proceedings / / edited by Sungdeok Cha, Jin-Young Choi, Moonzoo Kim, Mahesh Viswanathan |
| Edizione | [1st ed. 2008.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2008 |
| Descrizione fisica | 1 online resource (XIV, 430 p.) |
| Disciplina | 004.015113 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Computer networks
Computer science Computers, Special purpose Software engineering Compilers (Computer programs) Computer Communication Networks Computer Science Logic and Foundations of Programming Special Purpose and Application-Based Systems Software Engineering Compilers and Interpreters |
| ISBN | 3-540-88387-8 |
| Classificazione | 54.52 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- Tests, Proofs and Refinements -- Formal Verification and Biology -- Trust and Automation in Verification Tools -- Model Checking -- CTL Model-Checking with Graded Quantifiers -- Genetic Programming and Model Checking: Synthesizing New Mutual Exclusion Algorithms -- Computation Tree Regular Logic for Genetic Regulatory Networks -- Compositional Verification for Component-Based Systems and Application -- A Direct Algorithm for Multi-valued Bounded Model Checking -- Software Verification -- Model Checking Recursive Programs with Exact Predicate Abstraction -- Loop Summarization Using Abstract Transformers -- Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions -- Decision Procedures -- Automating Algebraic Specifications of Non-freely Generated Data Types -- Interpolants for Linear Arithmetic in SMT -- SAT Modulo ODE: A Direct SAT Approach to Hybrid Systems -- SMELS: Satisfiability Modulo Equality with Lazy Superposition -- Linear-Time Analysis -- Controllable Test Cases for the Distributed Test Architecture -- Tool Demonstration Papers -- Goanna: Syntactic Software Model Checking -- A Dynamic Assertion-Based Verification Platform for Validation of UML Designs -- CheckSpec: A Tool for Consistency and Coverage Analysis of Assertion Specifications -- DiVinE Multi-Core – A Parallel LTL Model-Checker -- Alaska -- NetQi: A Model Checker for Anticipation Game -- Component-Based Design and Analysis of Embedded Systems with UPPAAL PORT -- Timed and Stochastic Systems -- Time-Progress Evaluation for Dense-Time Automata with Concave Path Conditions -- Decidable Compositions of O-Minimal Automata -- On the Applicability of Stochastic Petri Nets for Analysis of Multiserver Retrial Systems with Different Vacation Policies -- Model Based Importance Analysis for Minimal CutSets -- Theory -- Approximate Invariant Property Checking Using Term-Height Reduction for a Subset of First-Order Logic -- Tree Pattern Rewriting Systems -- Deciding Bisimilarity of Full BPA Processes Locally -- Optimal Strategy Synthesis in Request-Response Games -- Short Papers -- Authentication Revisited: Flaw or Not, the Recursive Authentication Protocol -- Impartial Anticipation in Runtime-Verification -- Run-Time Monitoring of Electronic Contracts -- Practical Efficient Modular Linear-Time Model-Checking -- Passive Testing of Timed Systems. |
| Record Nr. | UNINA-9910768461503321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2008 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Automated Technology for Verification and Analysis : Third International Symposium, ATVA 2005, Taipei, Taiwan, October 4-7, 2005, Proceedings / / edited by Doron A. Peled, Yih-Kuen Tsay
| Automated Technology for Verification and Analysis : Third International Symposium, ATVA 2005, Taipei, Taiwan, October 4-7, 2005, Proceedings / / edited by Doron A. Peled, Yih-Kuen Tsay |
| Edizione | [1st ed. 2005.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2005 |
| Descrizione fisica | 1 online resource (XII, 508 p.) |
| Disciplina | 620.00420285 |
| Altri autori (Persone) |
PeledDoron A. <1962->
TsayYih-Kuen <1962-> |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Computer-aided engineering
Computer science Computer networks Computers, Special purpose Software engineering Compilers (Computer programs) Computer-Aided Engineering (CAD, CAE) and Design Computer Science Logic and Foundations of Programming Computer Communication Networks Special Purpose and Application-Based Systems Software Engineering Compilers and Interpreters |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Keynote Speeches -- Ranking Abstraction as a Companion to Predicate Abstraction -- Termination and Invariance Analysis of Loops -- Some Perspectives of Infinite-State Verification -- Model Checking -- Verifying Very Large Industrial Circuits Using 100 Processes and Beyond -- A New Reachability Algorithm for Symmetric Multi-processor Architecture -- Comprehensive Verification Framework for Dependability of Self-optimizing Systems -- Exploiting Hub States in Automatic Verification -- Combined Methods -- An Approach for the Verification of SystemC Designs Using AsmL -- Decomposition-Based Verification of Cyclic Workflows -- Timed, Embedded, and Hybrid Systems (I) -- Guaranteed Termination in the Verification of LTL Properties of Non-linear Robust Discrete Time Hybrid Systems -- Computation Platform for Automatic Analysis of Embedded Software Systems Using Model Based Approach -- Quantitative and Qualitative Analysis of Temporal Aspects of Complex Activities -- Automatic Test Case Generation with Region-Related Coverage Annotations for Real-Time Systems -- Abstraction and Reduction Techniques -- Selective Search in Bounded Model Checking of Reachability Properties -- Predicate Abstraction of RTL Verilog Descriptions Using Constraint Logic Programming -- State Space Exploration of Object-Based Systems Using Equivalence Reduction and the Sweepline Method -- Syntactical Colored Petri Nets Reductions -- Decidability and Complexity -- Algorithmic Algebraic Model Checking II: Decidability of Semi-algebraic Model Checking and Its Applications to Systems Biology -- A Static Analysis Using Tree Automata for XML Access Control -- Reasoning About Transfinite Sequences -- Semi-automatic Distributed Synthesis -- Established Formalisms and Standards -- A New Graph of Classes for the Preservation of Quantitative Temporal Constraints -- Comparison of Different Semantics for Time Petri Nets -- Introducing Dynamic Properties with Past Temporal Operators in the B Refinement -- Approximate Reachability for Dead Code Elimination in Esterel??? -- Compositional Verification and Games -- Synthesis of Interface Automata -- Multi-valued Model Checking Games -- Timed, Embedded, and Hybrid Systems (II) -- Model Checking Prioritized Timed Automata -- An MTBDD-Based Implementation of Forward Reachability for Probabilistic Timed Automata -- Protocols Analysis, Case Studies, and Tools -- An EFSM-Based Intrusion Detection System for Ad Hoc Networks -- Modeling and Verification of a Telecommunication Application Using Live Sequence Charts and the Play-Engine Tool -- Formal Construction and Verification of Home Service Robots: A Case Study -- Model Checking Real Time Java Using Java PathFinder -- Infinite-State and Parameterized Systems -- Using Parametric Automata for the Verification of the Stop-and-Wait Class of Protocols -- Flat Acceleration in Symbolic Model Checking -- Flat Counter Automata Almost Everywhere!. |
| Record Nr. | UNINA-9910483059003321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2005 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
The B Language and Method : A Guide to Practical Formal Development / / by Kevin Lano
| The B Language and Method : A Guide to Practical Formal Development / / by Kevin Lano |
| Autore | Lano Kevin |
| Edizione | [1st ed. 1996.] |
| Pubbl/distr/stampa | London : , : Springer London : , : Imprint : Springer, , 1996 |
| Descrizione fisica | 1 online resource (VIII, 232 p.) |
| Disciplina | 005.1/2/015113 |
| Collana | Formal Approaches to Computing and Information Technology (FACIT) |
| Soggetto topico |
Software engineering
Machine theory Compilers (Computer programs) Software Engineering Formal Languages and Automata Theory Compilers and Interpreters |
| ISBN | 1-4471-1494-9 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | 1 Introduction -- 1.1 Formal Methods -- 1.2 The History of B -- 1.3 The Relationship of B to Other Formal Methods -- 1.4 Summary -- 2 The Foundations of B AMN -- 2.1 Mathematical Notation -- 2.2 Defining Operations -- 2.3 Abstract Machines -- 2.4 Machine Composition Mechanisms -- 2.5 Refinement -- 2.6 Implementation -- 2.7 Summary -- 2.8 Exercises 1 -- 3 Analysis and Specification -- 3.1 Requirements Analysis -- 3.2 Specification Development -- 3.3 Animation -- 3.4 Proof of Internal Consistency Obligations -- 3.5 Ship Loading Case Study — Specification -- 3.6 Renaming -- 3.7 Aggregation -- 3.8 Summary -- 3.9 Exercises 2 -- 4 Design and Implementation -- 4.1 The Layered Development Paradigm -- 4.2 Refinement Examples -- 4.3 Proofs of Refinement -- 4.4 Decomposing Implementations -- 4.5 Ship Loading Case Study — Implementation -- 4.6 Summary -- 4.7 Exercises 3 -- 5 Case Studies -- 5.1 Personnel System Development -- 5.2 Mine Pump Control -- 5.3 Vending Machine -- 6 Conclusions -- A Exercise Solutions -- A.1 Exercises 1 -- A.2 Exercises 2 -- A.3 Exercises 3 -- B Properties of Weakest Preconditions -- B.1 Termination and Feasibility -- B.2 Set-theoretic Semantics -- B.3 Refinement -- B.4 Well-formedness Obligations -- B.5 Normal Forms -- B.6 Rules for ? -- B.7 Definition of := -- C Proof Techniques. |
| Record Nr. | UNINA-9911103106203321 |
Lano Kevin
|
||
| London : , : Springer London : , : Imprint : Springer, , 1996 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Bayesian Networks in R : with Applications in Systems Biology / / by Radhakrishnan Nagarajan, Marco Scutari, Sophie Lèbre
| Bayesian Networks in R : with Applications in Systems Biology / / by Radhakrishnan Nagarajan, Marco Scutari, Sophie Lèbre |
| Autore | Nagarajan Radhakrishnan |
| Edizione | [1st ed. 2013.] |
| Pubbl/distr/stampa | New York, NY : , : Springer New York : , : Imprint : Springer, , 2013 |
| Descrizione fisica | 1 online resource (168 p.) |
| Disciplina | 519.542 |
| Altri autori (Persone) |
ScutariMarco
LèbreSophie |
| Collana | Use R! |
| Soggetto topico |
Mathematical statistics - Data processing
Statistics Compilers (Computer programs) Statistics and Computing Statistical Theory and Methods Compilers and Interpreters |
| ISBN |
9781461464464
1461464463 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Introduction -- Bayesian Networks in the Absence of Temporal Information -- Bayesian Networds in the Presence of Temporal Information -- Bayesian Network Inference Algorithms -- Parallel Computing for Bayesian Networks -- Solutions -- Index -- References. |
| Record Nr. | UNINA-9910438136003321 |
|
Nagarajan Radhakrishnan
|
||
| New York, NY : , : Springer New York : , : Imprint : Springer, , 2013 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Soggetto topico
- Compilers (Computer programs) (1501)
-
Compilers and Interpreters
(1501)
- Computer science (1047)
- Software Engineering (1041)
- Software engineering (1041)