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 [[electronic resource] ] : 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 [[electronic resource] ] : 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 |
Programming languages (Electronic computers)
Computer logic Mathematical logic Artificial intelligence Computer programming Programming Languages, Compilers, Interpreters Logics and Meanings of Programs Mathematical Logic and Formal Languages 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. | UNISA-996466290303316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
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 |
Programming languages (Electronic computers)
Computer logic Mathematical logic Artificial intelligence Computer programming Programming Languages, Compilers, Interpreters Logics and Meanings of Programs Mathematical Logic and Formal Languages 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 | ||
| ||
Fields of Logic and Computation II [[electronic resource] ] : Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday / / edited by Lev D. Beklemishev, Andreas Blass, Nachum Dershowitz, Bernd Finkbeiner, Wolfram Schulte
| Fields of Logic and Computation II [[electronic resource] ] : Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday / / edited by Lev D. Beklemishev, Andreas Blass, Nachum Dershowitz, Bernd Finkbeiner, Wolfram Schulte |
| Edizione | [1st ed. 2015.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 |
| Descrizione fisica | 1 online resource (X, 319 p. 15 illus.) |
| Disciplina | 004.015113 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Computer programming
Programming Techniques |
| ISBN | 3-319-23534-6 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Preface -- Contents -- K-trivial, K-low and MLR-low Sequences: A Tutorial -- 1 Notation -- 2 K-trivial Sets: Definition and Existence -- 3 K-trivial and K-low Sequences -- 4 K-trivial Sequences Cannot Compute 0' -- 5 K-trivial Sequences Are K-low -- 6 K-low and MLR-low Oracles -- References -- Horn Clause Solvers for Program Verification -- 1 Introduction -- 1.1 Program Logics and Horn Clauses -- 1.2 Paper Outline -- 2 Horn Clause Basics -- 2.1 Existential Fixed-Point Logic and Horn Clauses -- 2.2 Derivations and Interpretations -- 2.3 Loose Semantics and Horn Clauses -- 3 From Programs to Clauses -- 3.1 State Machines -- 3.2 Procedural Languages -- 3.3 Proof Rules -- 4 Solving Horn Clauses -- 4.1 Magic Sets -- 4.2 Fold/Unfold -- 4.3 A Program Transformation for Inlining Assertions -- 5 Conclusions and Continuations -- References -- Existential Fixed-Point Logic as a Fragment of Second-Order Logic -- 1 Introduction -- 2 Preliminaries -- 2.1 Existential Fixed-Point Logic -- 2.2 Translation to Second-Order Logic -- 3 Model-Checking -- 4 Conjunctions -- 5 Satisfiability and Trimming -- 6 Trimming to Horn Form -- 7 Summary -- References -- On the Unpredictability of Individual Quantum Measurement Outcomes -- 1 Introduction -- 2 Models of Prediction -- 3 A Model for Prediction of Individual Physical Events -- 4 Computability Theoretic Notions of Unpredictability -- 5 Quantum Unpredictability -- 5.1 The Intuition of Quantum Indeterminism and Unpredictability -- 5.2 A Formal Basis for Quantum Indeterminism -- 5.3 Contextual Alternatives -- 5.4 Unpredictability of Individual Quantum Measurements -- 6 Incomputability, Unpredictability, and Quantum Randomness -- 7 Summary -- References -- The Ehrenfeucht-Fraïssé Method and the Planted Clique Conjecture -- 1 Introduction -- 2 Preliminaries -- 3 The Ehrenfeucht-Fraïssé-method.
4 A Logical Reformulation of ¶=NP -- 5 On Random (3-Col,LFP)-Sequences -- 6 The Planted Clique Conjecture -- 7 The Planted Clique Conjecture and (3-Col,LFP)-sequences -- 8 Some Remarks on the Logic Version of the Planted Clique Conjecture -- 9 Further Results and Open Questions -- References -- Monadic Theory of a Linear Order Versus the Theory of its Subsets with the Lifted Min/Max Operations -- 1 Introduction -- 2 Preliminaries -- 2.1 Linear Orders -- 2.2 Logical Structures -- 3 Lifted Structure -- 3.1 The Semigroup "426830A P(L), "3222378 "526930B -- 3.2 A Characterization of the Operation "3222378 -- 3.3 The Partially Ordered Set "426830A P(L), "526930B -- 3.4 Final Segments -- 3.5 A Characterization of the Ordering -- 4 Defining Single Elements -- 4.1 Immediate Predecessors -- 4.2 Singleton Sets -- 4.3 Recovering the Linear Order -- 4.4 Pairs -- 5 Defining Membership -- 5.1 Defining Final Segments -- 5.2 Upwards Closure -- 5.3 Membership When L has a Minimum Element 0 -- 5.4 Membership in the General Case -- 6 Final Proofs -- 6.1 Defining the Downarrow Operation with Uparrow -- 6.2 Defining the Uparrow Operation with the Order -- 6.3 Equivalent First-Order Structures -- References -- Regularity Equals Monadic Second-Order Definability for Quasi-trees -- 1 Introduction -- 2 Definitions, Notation and Basic Facts -- 2.1 Finite and Infinite Terms -- 2.2 Arrangements -- 2.3 Trees and Rooted Trees -- 2.4 Join-Trees -- 2.5 The Rank-Width of a Countable Graph -- 3 The Algebra of Binary Join-Trees -- 4 Quasi-trees -- References -- Capturing MSO with One Quantifier -- 1 Introduction -- 2 Preliminaries -- 3 Satisfiability Quantifier -- 4 Capturing MSO -- 5 Unranked Trees -- 6 Conclusion -- References -- Logics for Weighted Timed Pushdown Automata -- 1 Introduction -- 2 Weighted Timed Pushdown Automata -- 3 Weighted Timed Matching Logic. 4 Visibly Pushdown Languages -- 5 Decomposition of Weighted Timed Pushdown Automata -- 6 Definability Equals Recognizability -- 7 Weighted Timed Pushdown Automata with Global Clocks -- 8 Conclusion -- References -- Inherent Vacuity in Lattice Automata -- 1 Introduction -- 2 Preliminaries -- 2.1 Lattices -- 2.2 Lattice Automata -- 3 Vacuity in Lattice Automata -- 4 Useful Observations on Tolerance and Flexibility -- 4.1 Full-Order LDFW -- 4.2 Full-Order LNFW -- 4.3 Partial-Order LDFW -- 4.4 Partial-Order LNFW -- 5 Complexity of the Decision Problems -- 6 Inherent Vacuity with Analogy to Temporal Logic -- References -- Is Polynomial Time Choiceless? -- 1 Introduction -- 2 Choiceless Polynomial Time -- 2.1 BGS-Logic -- 2.2 Definition of Choiceless Polynomial Time -- 2.3 Defining Properties of Small Substructures -- 2.4 Choiceless Polynomial Time Without Counting -- 3 Fixed-Point Logic with Counting -- 4 Structures of Bounded Colour Class Size -- 5 Symmetric Circuits -- 6 Interpretation Logic -- 7 Challenges for Future Research -- 7.1 A Characterization Without Explicit Polynomial Bounds -- 7.2 Polynomial-Time Properties of Small Definable Subgraphs -- 7.3 Isomorphism of CFI-Graphs and Graphs of Bounded Colour Class Size -- 7.4 Constraint Satisfaction Problems -- 7.5 A Notion of Symmetric Circuits for CPT -- 7.6 Choiceless Polynomial Time versus Rank Logic -- References -- Arithmetical Congruence Preservation: From Finite to Infinite -- 1 Introduction -- 2 Switching Between Finite and Infinite -- 2.1 Lifting Functions Z/nZZ/mZ to NN and ZZ -- 2.2 Representation of Congruence Preserving Functions Z/nZZ/mZ -- 2.3 Lifting Functions Z/nZZ/mZ to Z/rZZ/sZ -- 3 Congruence Preservation on p-adic/profinite Integers -- 3.1 Congruence Preserving Functions Are Continuous -- 3.2 Congruence Preserving Functions and Inverse Limits. 3.3 Extension of Congruence Preserving Functions NN -- 3.4 Representation of Congruence Preserving Functions ZpZp -- 4 Conclusion -- References -- An Extension of the Ehrenfeucht-Fraïssé Game for First Order Logics Augmented with Lindström Quantifiers -- 1 Introduction -- 2 The Game -- 2.1 Description of the First Game -- 2.2 A Game Where Definability is Not Forced -- 2.3 A Game with Fixed Game-Board and Fixed Roles -- 3 Summary -- References -- Logics of Finite Hankel Rank -- 1 Introduction -- 1.1 Yuri's Quest for Logics for Computer Science -- 1.2 Preservation Theorems -- 1.3 Reduction Theorems -- 1.4 Purpose of This Paper -- 2 Background -- 2.1 Logics with Quantifier Rank -- 2.2 Sum-Like and Product-Like Operations on -structures -- 2.3 Abstract Lindström Logics -- 3 Hankel Matrices of -properties -- 3.1 Hankel Matrices -- 3.2 -Properties of Finite -rank -- 3.3 Proof of Theorem 5 -- 3.4 Properties of Finite S-rank and Finite P-rank -- 4 Hankel Matrices and the Feferman-Vaught Theorem -- 4.1 The FV-property -- 4.2 The FV-property and Finite Rank -- 5 The S-Closure of a Nice Logic -- 6 Conclusions and Open Problems -- References -- The Strategy of Campaigning -- 1 Introduction -- 2 A General Theorem -- 3 Ambiguity and Pessimism -- 4 The Logical Formalism of Dean and Parikh -- 5 Extension of the Framework -- 5.1 Candidate Beliefs -- 5.2 Stay-At-Home Voters -- 6 Conclusions and Future Work -- References -- On Almost Future Temporal Logics -- 1 Introduction -- 2 Preliminaries -- 2.1 First-Order Monadic Logic of Order -- 2.2 Propositional Temporal Logics -- 2.3 Kamp's and Stavi's Theorems -- 3 Future and Almost Future Formulas -- 4 No Finite Base for Almost Future Formulas -- 4.1 Proof of Lemma 4.3 -- 4.2 Proof of Lemma 4.4 -- 4.3 A Generalization -- References -- Minsky Machines and Algorithmic Problems -- 1 Introduction. 2 Turing Machines and Minsky Machines -- 2.1 Turing Machines -- 2.2 Minsky Machines -- 3 The Three Main Semigroups Simulating Minsky Machines -- 4 Varieties of Semigroups and the Word Problem -- 5 Gurevich's Theorem. The Uniform Word Problem for Finite Semigroups -- 6 The Uniform Word Problem for Finite Groups -- 6.1 Slobodskoi's Theorem -- 6.2 Some Applications of Slobodskoi's Theorem -- 7 Other Algorithmic Applications of Minsky Machines -- 7.1 Collatz Type Problems -- 7.2 Amalgams of Finite Semigroups -- 7.3 Complicated Residually Finite Semigroups -- References -- On Failure of 0-1 Laws -- References -- Composition Over the Natural Number Ordering with an Extra Binary Relation -- 1 Introduction -- 2 (N, <, P) with Monadic P -- 3 (N, <, R) with Binary R of Finite Valency -- 4 Applications -- 5 Conclusion -- References -- The Fundamental Nature of the Log Loss Function -- 1 Introduction -- 2 Loss Functions -- 3 Repetitive Predictions -- 4 A Simple Statement of Fundamentality -- 5 A Criterion of Fundamentality -- 6 Frequently Asked Questions -- 7 Conclusion -- References -- Erratum to: The Fundamental Natureof the Log Loss Function -- Author Index. |
| Record Nr. | UNISA-996466457103316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Fields of Logic and Computation II : Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday / / edited by Lev D. Beklemishev, Andreas Blass, Nachum Dershowitz, Bernd Finkbeiner, Wolfram Schulte
| Fields of Logic and Computation II : Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday / / edited by Lev D. Beklemishev, Andreas Blass, Nachum Dershowitz, Bernd Finkbeiner, Wolfram Schulte |
| Edizione | [1st ed. 2015.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 |
| Descrizione fisica | 1 online resource (X, 319 p. 15 illus.) |
| Disciplina | 004.015113 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Computer programming
Programming Techniques |
| ISBN | 3-319-23534-6 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Preface -- Contents -- K-trivial, K-low and MLR-low Sequences: A Tutorial -- 1 Notation -- 2 K-trivial Sets: Definition and Existence -- 3 K-trivial and K-low Sequences -- 4 K-trivial Sequences Cannot Compute 0' -- 5 K-trivial Sequences Are K-low -- 6 K-low and MLR-low Oracles -- References -- Horn Clause Solvers for Program Verification -- 1 Introduction -- 1.1 Program Logics and Horn Clauses -- 1.2 Paper Outline -- 2 Horn Clause Basics -- 2.1 Existential Fixed-Point Logic and Horn Clauses -- 2.2 Derivations and Interpretations -- 2.3 Loose Semantics and Horn Clauses -- 3 From Programs to Clauses -- 3.1 State Machines -- 3.2 Procedural Languages -- 3.3 Proof Rules -- 4 Solving Horn Clauses -- 4.1 Magic Sets -- 4.2 Fold/Unfold -- 4.3 A Program Transformation for Inlining Assertions -- 5 Conclusions and Continuations -- References -- Existential Fixed-Point Logic as a Fragment of Second-Order Logic -- 1 Introduction -- 2 Preliminaries -- 2.1 Existential Fixed-Point Logic -- 2.2 Translation to Second-Order Logic -- 3 Model-Checking -- 4 Conjunctions -- 5 Satisfiability and Trimming -- 6 Trimming to Horn Form -- 7 Summary -- References -- On the Unpredictability of Individual Quantum Measurement Outcomes -- 1 Introduction -- 2 Models of Prediction -- 3 A Model for Prediction of Individual Physical Events -- 4 Computability Theoretic Notions of Unpredictability -- 5 Quantum Unpredictability -- 5.1 The Intuition of Quantum Indeterminism and Unpredictability -- 5.2 A Formal Basis for Quantum Indeterminism -- 5.3 Contextual Alternatives -- 5.4 Unpredictability of Individual Quantum Measurements -- 6 Incomputability, Unpredictability, and Quantum Randomness -- 7 Summary -- References -- The Ehrenfeucht-Fraïssé Method and the Planted Clique Conjecture -- 1 Introduction -- 2 Preliminaries -- 3 The Ehrenfeucht-Fraïssé-method.
4 A Logical Reformulation of ¶=NP -- 5 On Random (3-Col,LFP)-Sequences -- 6 The Planted Clique Conjecture -- 7 The Planted Clique Conjecture and (3-Col,LFP)-sequences -- 8 Some Remarks on the Logic Version of the Planted Clique Conjecture -- 9 Further Results and Open Questions -- References -- Monadic Theory of a Linear Order Versus the Theory of its Subsets with the Lifted Min/Max Operations -- 1 Introduction -- 2 Preliminaries -- 2.1 Linear Orders -- 2.2 Logical Structures -- 3 Lifted Structure -- 3.1 The Semigroup "426830A P(L), "3222378 "526930B -- 3.2 A Characterization of the Operation "3222378 -- 3.3 The Partially Ordered Set "426830A P(L), "526930B -- 3.4 Final Segments -- 3.5 A Characterization of the Ordering -- 4 Defining Single Elements -- 4.1 Immediate Predecessors -- 4.2 Singleton Sets -- 4.3 Recovering the Linear Order -- 4.4 Pairs -- 5 Defining Membership -- 5.1 Defining Final Segments -- 5.2 Upwards Closure -- 5.3 Membership When L has a Minimum Element 0 -- 5.4 Membership in the General Case -- 6 Final Proofs -- 6.1 Defining the Downarrow Operation with Uparrow -- 6.2 Defining the Uparrow Operation with the Order -- 6.3 Equivalent First-Order Structures -- References -- Regularity Equals Monadic Second-Order Definability for Quasi-trees -- 1 Introduction -- 2 Definitions, Notation and Basic Facts -- 2.1 Finite and Infinite Terms -- 2.2 Arrangements -- 2.3 Trees and Rooted Trees -- 2.4 Join-Trees -- 2.5 The Rank-Width of a Countable Graph -- 3 The Algebra of Binary Join-Trees -- 4 Quasi-trees -- References -- Capturing MSO with One Quantifier -- 1 Introduction -- 2 Preliminaries -- 3 Satisfiability Quantifier -- 4 Capturing MSO -- 5 Unranked Trees -- 6 Conclusion -- References -- Logics for Weighted Timed Pushdown Automata -- 1 Introduction -- 2 Weighted Timed Pushdown Automata -- 3 Weighted Timed Matching Logic. 4 Visibly Pushdown Languages -- 5 Decomposition of Weighted Timed Pushdown Automata -- 6 Definability Equals Recognizability -- 7 Weighted Timed Pushdown Automata with Global Clocks -- 8 Conclusion -- References -- Inherent Vacuity in Lattice Automata -- 1 Introduction -- 2 Preliminaries -- 2.1 Lattices -- 2.2 Lattice Automata -- 3 Vacuity in Lattice Automata -- 4 Useful Observations on Tolerance and Flexibility -- 4.1 Full-Order LDFW -- 4.2 Full-Order LNFW -- 4.3 Partial-Order LDFW -- 4.4 Partial-Order LNFW -- 5 Complexity of the Decision Problems -- 6 Inherent Vacuity with Analogy to Temporal Logic -- References -- Is Polynomial Time Choiceless? -- 1 Introduction -- 2 Choiceless Polynomial Time -- 2.1 BGS-Logic -- 2.2 Definition of Choiceless Polynomial Time -- 2.3 Defining Properties of Small Substructures -- 2.4 Choiceless Polynomial Time Without Counting -- 3 Fixed-Point Logic with Counting -- 4 Structures of Bounded Colour Class Size -- 5 Symmetric Circuits -- 6 Interpretation Logic -- 7 Challenges for Future Research -- 7.1 A Characterization Without Explicit Polynomial Bounds -- 7.2 Polynomial-Time Properties of Small Definable Subgraphs -- 7.3 Isomorphism of CFI-Graphs and Graphs of Bounded Colour Class Size -- 7.4 Constraint Satisfaction Problems -- 7.5 A Notion of Symmetric Circuits for CPT -- 7.6 Choiceless Polynomial Time versus Rank Logic -- References -- Arithmetical Congruence Preservation: From Finite to Infinite -- 1 Introduction -- 2 Switching Between Finite and Infinite -- 2.1 Lifting Functions Z/nZZ/mZ to NN and ZZ -- 2.2 Representation of Congruence Preserving Functions Z/nZZ/mZ -- 2.3 Lifting Functions Z/nZZ/mZ to Z/rZZ/sZ -- 3 Congruence Preservation on p-adic/profinite Integers -- 3.1 Congruence Preserving Functions Are Continuous -- 3.2 Congruence Preserving Functions and Inverse Limits. 3.3 Extension of Congruence Preserving Functions NN -- 3.4 Representation of Congruence Preserving Functions ZpZp -- 4 Conclusion -- References -- An Extension of the Ehrenfeucht-Fraïssé Game for First Order Logics Augmented with Lindström Quantifiers -- 1 Introduction -- 2 The Game -- 2.1 Description of the First Game -- 2.2 A Game Where Definability is Not Forced -- 2.3 A Game with Fixed Game-Board and Fixed Roles -- 3 Summary -- References -- Logics of Finite Hankel Rank -- 1 Introduction -- 1.1 Yuri's Quest for Logics for Computer Science -- 1.2 Preservation Theorems -- 1.3 Reduction Theorems -- 1.4 Purpose of This Paper -- 2 Background -- 2.1 Logics with Quantifier Rank -- 2.2 Sum-Like and Product-Like Operations on -structures -- 2.3 Abstract Lindström Logics -- 3 Hankel Matrices of -properties -- 3.1 Hankel Matrices -- 3.2 -Properties of Finite -rank -- 3.3 Proof of Theorem 5 -- 3.4 Properties of Finite S-rank and Finite P-rank -- 4 Hankel Matrices and the Feferman-Vaught Theorem -- 4.1 The FV-property -- 4.2 The FV-property and Finite Rank -- 5 The S-Closure of a Nice Logic -- 6 Conclusions and Open Problems -- References -- The Strategy of Campaigning -- 1 Introduction -- 2 A General Theorem -- 3 Ambiguity and Pessimism -- 4 The Logical Formalism of Dean and Parikh -- 5 Extension of the Framework -- 5.1 Candidate Beliefs -- 5.2 Stay-At-Home Voters -- 6 Conclusions and Future Work -- References -- On Almost Future Temporal Logics -- 1 Introduction -- 2 Preliminaries -- 2.1 First-Order Monadic Logic of Order -- 2.2 Propositional Temporal Logics -- 2.3 Kamp's and Stavi's Theorems -- 3 Future and Almost Future Formulas -- 4 No Finite Base for Almost Future Formulas -- 4.1 Proof of Lemma 4.3 -- 4.2 Proof of Lemma 4.4 -- 4.3 A Generalization -- References -- Minsky Machines and Algorithmic Problems -- 1 Introduction. 2 Turing Machines and Minsky Machines -- 2.1 Turing Machines -- 2.2 Minsky Machines -- 3 The Three Main Semigroups Simulating Minsky Machines -- 4 Varieties of Semigroups and the Word Problem -- 5 Gurevich's Theorem. The Uniform Word Problem for Finite Semigroups -- 6 The Uniform Word Problem for Finite Groups -- 6.1 Slobodskoi's Theorem -- 6.2 Some Applications of Slobodskoi's Theorem -- 7 Other Algorithmic Applications of Minsky Machines -- 7.1 Collatz Type Problems -- 7.2 Amalgams of Finite Semigroups -- 7.3 Complicated Residually Finite Semigroups -- References -- On Failure of 0-1 Laws -- References -- Composition Over the Natural Number Ordering with an Extra Binary Relation -- 1 Introduction -- 2 (N, <, P) with Monadic P -- 3 (N, <, R) with Binary R of Finite Valency -- 4 Applications -- 5 Conclusion -- References -- The Fundamental Nature of the Log Loss Function -- 1 Introduction -- 2 Loss Functions -- 3 Repetitive Predictions -- 4 A Simple Statement of Fundamentality -- 5 A Criterion of Fundamentality -- 6 Frequently Asked Questions -- 7 Conclusion -- References -- Erratum to: The Fundamental Natureof the Log Loss Function -- Author Index. |
| Record Nr. | UNINA-9910484001403321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Fields of Logic and Computation III [[electronic resource] ] : Essays Dedicated to Yuri Gurevich on the Occasion of His 80th Birthday / / edited by Andreas Blass, Patrick Cégielski, Nachum Dershowitz, Manfred Droste, Bernd Finkbeiner
| Fields of Logic and Computation III [[electronic resource] ] : Essays Dedicated to Yuri Gurevich on the Occasion of His 80th Birthday / / edited by Andreas Blass, Patrick Cégielski, Nachum Dershowitz, Manfred Droste, Bernd Finkbeiner |
| Edizione | [1st ed. 2020.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2020 |
| Descrizione fisica | 1 online resource (x, 341 pages) |
| Disciplina | 004.015113 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Computer programming
Data structures (Computer science) Computer communication systems Special purpose computers Artificial intelligence Computer logic Software engineering Programming Techniques Data Structures Computer Communication Networks Special Purpose and Application-Based Systems Logic in AI Software Engineering |
| ISBN | 3-030-48006-2 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Computation -- Logic -- Verification -- Topos theory. -Parallel Computing -- Tree -- Gurevich conjecture -- Arabic algorithms -- Hyperbolic group -- Lattice-ordered group -- Temporal logic -- Metric logic -- Random convergence -- Knot theory -- Entropic convergence -- Random access machine, PTIME -- Algorithmic randomness. . |
| Record Nr. | UNISA-996418286403316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2020 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Fields of Logic and Computation III : Essays Dedicated to Yuri Gurevich on the Occasion of His 80th Birthday / / edited by Andreas Blass, Patrick Cégielski, Nachum Dershowitz, Manfred Droste, Bernd Finkbeiner
| Fields of Logic and Computation III : Essays Dedicated to Yuri Gurevich on the Occasion of His 80th Birthday / / edited by Andreas Blass, Patrick Cégielski, Nachum Dershowitz, Manfred Droste, Bernd Finkbeiner |
| Edizione | [1st ed. 2020.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2020 |
| Descrizione fisica | 1 online resource (x, 341 pages) |
| Disciplina |
004.015113
005.1015113 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Computer programming
Data structures (Computer science) Computer communication systems Special purpose computers Artificial intelligence Computer logic Software engineering Programming Techniques Data Structures Computer Communication Networks Special Purpose and Application-Based Systems Logic in AI Software Engineering |
| ISBN | 3-030-48006-2 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Computation -- Logic -- Verification -- Topos theory. -Parallel Computing -- Tree -- Gurevich conjecture -- Arabic algorithms -- Hyperbolic group -- Lattice-ordered group -- Temporal logic -- Metric logic -- Random convergence -- Knot theory -- Entropic convergence -- Random access machine, PTIME -- Algorithmic randomness. . |
| Record Nr. | UNINA-9910409668103321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2020 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Runtime Verification [[electronic resource] ] : 19th International Conference, RV 2019, Porto, Portugal, October 8–11, 2019, Proceedings / / edited by Bernd Finkbeiner, Leonardo Mariani
| Runtime Verification [[electronic resource] ] : 19th International Conference, RV 2019, Porto, Portugal, October 8–11, 2019, Proceedings / / edited by Bernd Finkbeiner, Leonardo Mariani |
| Edizione | [1st ed. 2019.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 |
| Descrizione fisica | 1 online resource (X, 413 p. 377 illus., 58 illus. in color.) |
| Disciplina | 005.14 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Software engineering
Programming languages (Electronic computers) Computer logic Computer system failures Algorithms Mathematical logic Software Engineering Programming Languages, Compilers, Interpreters Logics and Meanings of Programs System Performance and Evaluation Algorithm Analysis and Problem Complexity Mathematical Logic and Formal Languages |
| ISBN | 3-030-32079-0 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | A Retrospective Look at the Monitoring and Checking (MaC) Framework -- Introspective Environment Modeling -- Robustness of Specifications and its applications to Falsification, Parameter Mining, and Runtime Monitoring with S-TaLiRo -- On the Runtime Enforcement of Timed Properties -- Algorithms for Monitoring Hyperproperties -- Stream-based Monitors for Real-time Properties -- Accelerated Learning of Predictive Runtime Monitors for Rare Failure -- Neural Predictive Monitoring -- Comparing Controlled System Synthesis and Suppression Enforcement -- Assumption-Based Runtime Verification with Partial Observability and Resets -- Decentralized Stream Runtime Verification -- Explaining Violations of Properties in Control-Flow Temporal Logic -- FastCFI: Real-Time Control Flow Integrity using FPGA without Code Instrumentation -- An Extension of LTL with Rules and its Application to Runtime Verification -- Monitorability Over Unreliable Channels -- Runtime Verification For Timed Event Streams With Partial Information -- Shape Expressions for Specifying and Extracting Signal Features -- A Formally Verified Monitor for Metric First-Order Temporal Logic -- Efficient Detection and Quantification of Timing Leaks with Neural Networks -- Predictive Runtime Monitoring for Linear Stochastic Systems and Applications to Geofence Enforcement for UAVs -- Reactive Control Meets Runtime Verification: A Case Study of Navigation -- Overhead-aware deployment of runtime monitors -- NuRV: a nuXmv Extension for Runtime Verification -- AllenRV: an extensible monitor for multiple complex specifications with high reactivity -- Timescales: A Benchmark Generator for Metric Temporal Logic. |
| Record Nr. | UNISA-996466431103316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Runtime Verification : 19th International Conference, RV 2019, Porto, Portugal, October 8–11, 2019, Proceedings / / edited by Bernd Finkbeiner, Leonardo Mariani
| Runtime Verification : 19th International Conference, RV 2019, Porto, Portugal, October 8–11, 2019, Proceedings / / edited by Bernd Finkbeiner, Leonardo Mariani |
| Edizione | [1st ed. 2019.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 |
| Descrizione fisica | 1 online resource (X, 413 p. 377 illus., 58 illus. in color.) |
| Disciplina | 005.14 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Software engineering
Programming languages (Electronic computers) Computer logic Computer system failures Algorithms Mathematical logic Software Engineering Programming Languages, Compilers, Interpreters Logics and Meanings of Programs System Performance and Evaluation Algorithm Analysis and Problem Complexity Mathematical Logic and Formal Languages |
| ISBN | 3-030-32079-0 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | A Retrospective Look at the Monitoring and Checking (MaC) Framework -- Introspective Environment Modeling -- Robustness of Specifications and its applications to Falsification, Parameter Mining, and Runtime Monitoring with S-TaLiRo -- On the Runtime Enforcement of Timed Properties -- Algorithms for Monitoring Hyperproperties -- Stream-based Monitors for Real-time Properties -- Accelerated Learning of Predictive Runtime Monitors for Rare Failure -- Neural Predictive Monitoring -- Comparing Controlled System Synthesis and Suppression Enforcement -- Assumption-Based Runtime Verification with Partial Observability and Resets -- Decentralized Stream Runtime Verification -- Explaining Violations of Properties in Control-Flow Temporal Logic -- FastCFI: Real-Time Control Flow Integrity using FPGA without Code Instrumentation -- An Extension of LTL with Rules and its Application to Runtime Verification -- Monitorability Over Unreliable Channels -- Runtime Verification For Timed Event Streams With Partial Information -- Shape Expressions for Specifying and Extracting Signal Features -- A Formally Verified Monitor for Metric First-Order Temporal Logic -- Efficient Detection and Quantification of Timing Leaks with Neural Networks -- Predictive Runtime Monitoring for Linear Stochastic Systems and Applications to Geofence Enforcement for UAVs -- Reactive Control Meets Runtime Verification: A Case Study of Navigation -- Overhead-aware deployment of runtime monitors -- NuRV: a nuXmv Extension for Runtime Verification -- AllenRV: an extensible monitor for multiple complex specifications with high reactivity -- Timescales: A Benchmark Generator for Metric Temporal Logic. |
| Record Nr. | UNINA-9910349276103321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Runtime Verification [[electronic resource] ] : First International Conference, RV 2010, St. Julians, Malta, November 1-4, 2010. Proceedings / / edited by Howard Barringer, Ylies Falcone, Bernd Finkbeiner, Klaus Havelund, Insup Lee, Gordon Pace, Grigore Rosu, Oleg Sokolsky, Nikolai Tillmann
| Runtime Verification [[electronic resource] ] : First International Conference, RV 2010, St. Julians, Malta, November 1-4, 2010. Proceedings / / edited by Howard Barringer, Ylies Falcone, Bernd Finkbeiner, Klaus Havelund, Insup Lee, Gordon Pace, Grigore Rosu, Oleg Sokolsky, Nikolai Tillmann |
| Edizione | [1st ed. 2010.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2010 |
| Descrizione fisica | 1 online resource (XIII, 492 p. 145 illus.) |
| Disciplina | 005.1 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Software engineering
Algorithms Computer logic Computer programming Programming languages (Electronic computers) Software Engineering/Programming and Operating Systems Software Engineering Algorithm Analysis and Problem Complexity Logics and Meanings of Programs Programming Techniques Programming Languages, Compilers, Interpreters |
| ISBN |
1-280-39014-X
9786613568069 3-642-16612-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Papers -- Automatic Requirement Extraction from Test Cases -- Code Contracts for .NET: Runtime Verification and So Much More -- Visual Debugging for Stream Processing Applications -- Runtime Verification in Context: Can Optimizing Error Detection Improve Fault Diagnosis? -- Contracts for Scala -- Runtime Analysis and Instrumentation for Securing Software -- Tutorials -- Run-Time Verification of Networked Software -- Clara: Partially Evaluating Runtime Monitors at Compile Time -- You Should Better Enforce Than Verify -- Runtime Verification for the Web -- Statistical Model Checking: An Overview -- Runtime Verification with the RV System -- Regular and Short Papers -- A Meta-Aspect Protocol for Developing Dynamic Analyses -- Behavior Abstraction in Malware Analysis -- Clara: A Framework for Partially Evaluating Finite-State Runtime Monitors Ahead of Time -- Checking the Correspondence between UML Models and Implementation -- Compensation-Aware Runtime Monitoring -- Recovery Tasks: An Automated Approach to Failure Recovery -- Formally Efficient Program Instrumentation -- Interval Analysis for Concurrent Trace Programs Using Transaction Sequence Graphs -- Causality Analysis in Contract Violation -- Reducing Configurations to Monitor in a Software Product Line -- Runtime Instrumentation for Precise Flow-Sensitive Type Analysis -- Trace Recording for Embedded Systems: Lessons Learned from Five Industrial Projects -- Verification of an AFDX Infrastructure Using Simulations and Probabilities -- Copilot: A Hard Real-Time Runtime Monitor -- StealthWorks: Emulating Memory Errors -- Efficient Data Race Detection for Async-Finish Parallelism -- Run-Time Verification of Optimistic Concurrency -- Who Guards the Guardians? — Toward V&V of Health Management Software -- Aspect-Oriented Instrumentation with GCC -- Runtime Verification for Software Transactional Memories -- Optimized Temporal Monitors for SystemC -- Runtime Verification of Stochastic, Faulty Systems -- Low-Overhead Bug Fingerprinting for Fast Debugging -- Tool Demonstrations -- ESAT: A Tool for Animating Logic-Based Specifications of Evolvable Component Systems -- A Tool Which Mines Partial Execution Traces to Improve Static Analysis -- LarvaStat: Monitoring of Statistical Properties -- WS-PSC Monitor: A Tool Chain for Monitoring Temporal and Timing Properties in Composite Service Based on Property Sequence Chart. |
| Record Nr. | UNISA-996466238703316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2010 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Verification, Model Checking, and Abstract Interpretation [[electronic resource] ] : 23rd International Conference, VMCAI 2022, Philadelphia, PA, USA, January 16–18, 2022, Proceedings / / edited by Bernd Finkbeiner, Thomas Wies
| Verification, Model Checking, and Abstract Interpretation [[electronic resource] ] : 23rd International Conference, VMCAI 2022, Philadelphia, PA, USA, January 16–18, 2022, Proceedings / / edited by Bernd Finkbeiner, Thomas Wies |
| Edizione | [1st ed. 2022.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2022 |
| Descrizione fisica | 1 online resource (531 pages) |
| Disciplina | 005.3 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer science
Mathematical logic Artificial intelligence Computer networks Theory of Computation Mathematical Logic and Foundations Artificial Intelligence Computer Communication Networks |
| ISBN | 3-030-94583-9 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNISA-996464552403316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2022 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
