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.
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 | ||
| ||
FM 2011: Formal Methods [[electronic resource] ] : 17th International Symposium on Formal Methods, Limerick, Ireland, June 20-24, 2011, Proceedings / / edited by Michael Butler, Wolfram Schulte
| FM 2011: Formal Methods [[electronic resource] ] : 17th International Symposium on Formal Methods, Limerick, Ireland, June 20-24, 2011, Proceedings / / edited by Michael Butler, Wolfram Schulte |
| Edizione | [1st ed. 2011.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2011 |
| Descrizione fisica | 1 online resource (XIV, 450 p. 110 illus., 27 illus. in color.) |
| Disciplina | 005.1 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Software engineering
Computer logic Programming languages (Electronic computers) Computer programming Mathematical logic Management information systems Computer science Software Engineering Logics and Meanings of Programs Programming Languages, Compilers, Interpreters Programming Techniques Mathematical Logic and Formal Languages Management of Computing and Information Systems |
| ISBN | 3-642-21437-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Model integration and cyber physical systems: a semantics perspective / Janos Sztipanovits -- Some thoughts on behavioral programming / David Harel. |
| Record Nr. | UNISA-996465420503316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2011 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Formal Methods and Software Engineering [[electronic resource] ] : 6th International Conference on Formal Engineering Methods, ICFEM 2004, Seattle, WA, USA, November 8-12, 2004, Proceedings / / edited by Jim Davies, Wolfram Schulte, Mike Barnett
| Formal Methods and Software Engineering [[electronic resource] ] : 6th International Conference on Formal Engineering Methods, ICFEM 2004, Seattle, WA, USA, November 8-12, 2004, Proceedings / / edited by Jim Davies, Wolfram Schulte, Mike Barnett |
| Edizione | [1st ed. 2004.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 |
| Descrizione fisica | 1 online resource (IX, 500 p.) |
| Disciplina | 005.131 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Software engineering
Computer logic Programming languages (Electronic computers) Software Engineering/Programming and Operating Systems Software Engineering Logics and Meanings of Programs Programming Languages, Compilers, Interpreters |
| ISBN | 3-540-30482-7 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Tutorials -- Model-Based Development: Combining Engineering Approaches and Formal Techniques -- Tutorial on the RAISE Language, Method and Tools -- Model-Based Testing with Spec# -- Formal Engineering for Industrial Software Development – An Introduction to the SOFL Specification Language and Method -- Tutorial: Software Model Checking -- Invited Talks -- Engineering Quality Software -- When Can Formal Methods Make a Real Difference? -- On the Adoption of Formal Methods by Industry: The ACL2 Experience -- A CLP Approach to Modelling Systems -- Full Papers -- Multi-prover Verification of C Programs -- Memory-Model-Sensitive Data Race Analysis -- Formal Models for Web Navigations with Session Control and Browser Cache -- Managing Verification Activities Using SVM -- A General Model for Reachability Testing of Concurrent Programs -- A Knowledge Based Analysis of Cache Coherence -- A Propositional Logic-Based Method for Verification of Feature Models -- Deriving Probabilistic Semantics Via the ‘Weakest Completion’ -- CSP Representation of Game Semantics for Second-Order Idealized Algol -- An Equational Calculus for Alloy -- Guiding Spin Simulation -- Linear Inequality LTL (iLTL): A Model Checker for Discrete Time Markov Chains -- Software Model Checking Using Linear Constraints -- Counterexample Guided Abstraction Refinement Via Program Execution -- Faster Analysis of Formal Specifications -- Bridging Refinement of Interface Automata to Forward Simulation of I/O Automata -- Learning to Verify Safety Properties -- Automatic Extraction of Object-Oriented Observer Abstractions from Unit-Test Executions -- A Specification-Based Approach to Testing Polymorphic Attributes -- From Circus to JCSP -- An Approach to Preserve Protocol Consistency and Executability Across Updates -- A Formal Monitoring-Based Framework for Software Development and Analysis -- Verifying a File System Implementation -- Verifying the On-line Help System of SIEMENS Magnetic Resonance Tomographs -- Implementing Dynamic Aggregations of Abstract Machines in the B Method -- Formal Proof from UML Models -- Interactive Verification of UML State Machines -- Refinement of Actions for Real-Time Concurrent Systems with Causal Ambiguity -- From Durational Specifications to TLA Designs of Timed Automata -- Timed Patterns: TCOZ to Timed Automata. |
| Record Nr. | UNISA-996465497903316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Formal Methods and Software Engineering : 6th International Conference on Formal Engineering Methods, ICFEM 2004, Seattle, WA, USA, November 8-12, 2004, Proceedings / / edited by Jim Davies, Wolfram Schulte, Mike Barnett
| Formal Methods and Software Engineering : 6th International Conference on Formal Engineering Methods, ICFEM 2004, Seattle, WA, USA, November 8-12, 2004, Proceedings / / edited by Jim Davies, Wolfram Schulte, Mike Barnett |
| Edizione | [1st ed. 2004.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 |
| Descrizione fisica | 1 online resource (IX, 500 p.) |
| Disciplina | 005.131 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Software engineering
Computer logic Programming languages (Electronic computers) Software Engineering/Programming and Operating Systems Software Engineering Logics and Meanings of Programs Programming Languages, Compilers, Interpreters |
| ISBN | 3-540-30482-7 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Tutorials -- Model-Based Development: Combining Engineering Approaches and Formal Techniques -- Tutorial on the RAISE Language, Method and Tools -- Model-Based Testing with Spec# -- Formal Engineering for Industrial Software Development – An Introduction to the SOFL Specification Language and Method -- Tutorial: Software Model Checking -- Invited Talks -- Engineering Quality Software -- When Can Formal Methods Make a Real Difference? -- On the Adoption of Formal Methods by Industry: The ACL2 Experience -- A CLP Approach to Modelling Systems -- Full Papers -- Multi-prover Verification of C Programs -- Memory-Model-Sensitive Data Race Analysis -- Formal Models for Web Navigations with Session Control and Browser Cache -- Managing Verification Activities Using SVM -- A General Model for Reachability Testing of Concurrent Programs -- A Knowledge Based Analysis of Cache Coherence -- A Propositional Logic-Based Method for Verification of Feature Models -- Deriving Probabilistic Semantics Via the ‘Weakest Completion’ -- CSP Representation of Game Semantics for Second-Order Idealized Algol -- An Equational Calculus for Alloy -- Guiding Spin Simulation -- Linear Inequality LTL (iLTL): A Model Checker for Discrete Time Markov Chains -- Software Model Checking Using Linear Constraints -- Counterexample Guided Abstraction Refinement Via Program Execution -- Faster Analysis of Formal Specifications -- Bridging Refinement of Interface Automata to Forward Simulation of I/O Automata -- Learning to Verify Safety Properties -- Automatic Extraction of Object-Oriented Observer Abstractions from Unit-Test Executions -- A Specification-Based Approach to Testing Polymorphic Attributes -- From Circus to JCSP -- An Approach to Preserve Protocol Consistency and Executability Across Updates -- A Formal Monitoring-Based Framework for Software Development and Analysis -- Verifying a File System Implementation -- Verifying the On-line Help System of SIEMENS Magnetic Resonance Tomographs -- Implementing Dynamic Aggregations of Abstract Machines in the B Method -- Formal Proof from UML Models -- Interactive Verification of UML State Machines -- Refinement of Actions for Real-Time Concurrent Systems with Causal Ambiguity -- From Durational Specifications to TLA Designs of Timed Automata -- Timed Patterns: TCOZ to Timed Automata. |
| Record Nr. | UNINA-9910144336703321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Model-Driven Engineering Languages and Systems [[electronic resource] ] : 17th International Conference, MODELS 2014, Valencia, Spain, September 283– October 4, 2014. Proceedings / / edited by Juergen Dingel, Wolfram Schulte, Isidro Ramos, Silvia Abrahao, Emilio Insfran
| Model-Driven Engineering Languages and Systems [[electronic resource] ] : 17th International Conference, MODELS 2014, Valencia, Spain, September 283– October 4, 2014. Proceedings / / edited by Juergen Dingel, Wolfram Schulte, Isidro Ramos, Silvia Abrahao, Emilio Insfran |
| Edizione | [1st ed. 2014.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2014 |
| Descrizione fisica | 1 online resource (XXVIII, 688 p. 227 illus.) |
| Disciplina | 005.1 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Programming languages (Electronic computers)
Software engineering Computer logic Management information systems Computer science Computer simulation Computer system failures Programming Languages, Compilers, Interpreters Software Engineering Logics and Meanings of Programs Management of Computing and Information Systems Simulation and Modeling System Performance and Evaluation |
| ISBN | 3-319-11653-3 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Cloud, Mobile and Web Computing -- Model-Driven Development of Mobile Applications Allowing Role-Driven Variants -- A Model-Based System to Automate Cloud Resource Allocation and Optimization -- An Evaluation of the Effectiveness of the Atomic Section Model -- Model Transformation 1 -- Parsing in a Broad Sense -- Streaming Model Transformations by Complex Event Processing -- On the Use of Signatures for Source Incremental Model-to-text Transformation -- Behavioral Modeling -- Modeling Systemic Behavior by State-Based Holonic Modular Units -- Semantic Model Differencing Utilizing Behavioral Semantics Specifications -- Formalizing Execution Semantics of UML Profiles with fUML Models -- MDE: Past, Present and Future.-Who Knows/Uses What of the UML: A Personal Opinion Survey -- Assessing the State-of-Practice of Model-Based Engineering in the Embedded Systems Domain -- The Relevance of Model-Driven Engineering Thirty Years from Now -- Formal Semantics, Specification and Verification -- Verifying Compilation of Synchronous Distributed Applications -- Environment-Centric Contracts for Design of Cyber-Physical Systems -- Removing Redundancies and Deducing Equivalences in UML Class Diagrams -- Models at Runtime -- A Native Versioning Concept to Support Historized Models at Runtime -- Modelling Adaptation Policies as Domain-Specific Constraints -- Scalable Armies of Model Clones through Data Sharing -- Feature and Variability Modeling -- Three Cases of Feature-Based Variability Modeling in Industry -- Supporting Multiplicity and Hierarchy in Model-Based Configuration: Experiences and Lessons Learned -- Propagating Decisions to Detect and Explain Conflicts in a Multi-step Configuration Process -- Composition and Adaptation -- An MDA Approach for the Generation of Communication Adapters Integrating SW and FW Components from Simulink -- A UML Model-Driven Approach to Efficiently Allocate Complex Communication Schemes -- Model-Integrating Software Components -- Practices and Experience -- Experiences in Applying Model Driven Engineering to the Telescope and Instrument Control System Domain -- Model Driven Grant Proposal Engineering -- Agile Model-Driven Engineering in Mechatronic Systems - An Industrial Case Study -- Modeling for Analysis -- Using UML for Modeling Procedural Legal Rules: Approach and a Study of Luxembourg’s Tax Law -- Resolution of Interfering Product Fragments in Software Product Line Engineering -- Ontology-Based Modeling of Context-Aware Systems -- Pragmatics -- Comprehending Feature Models Expressed in CVL -- On the Impact of Layout Quality to Understanding UML Diagrams: Size Matters -- Enabling the Development of Cognitive Effective Visual DSLs -- Model Extraction, Manipulation and Persistence -- JUMP—From Java Annotations to UML Profiles -- SIGMA: Scala Internal Domain-Specific Languages for Model Manipulations -- A Framework to Benchmark NoSQL Data Stores for Large-Scale Model Persistence -- Model Transformation 2 -- Automated Chaining of Model Transformations with Incompatible Metamodels -- Classification of Model Transformation Tools: Pattern Matching Techniques -- Learning Implicit and Explicit Control in Model Transformations by Example -- Querying and Reasoning IncQuery-D: A Distributed Incremental Model Query Framework in the Cloud -- Translating OCL to Graph Patterns. |
| Record Nr. | UNISA-996199682703316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2014 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Model-Driven Engineering Languages and Systems : 17th International Conference, MODELS 2014, Valencia, Spain, September 283– October 4, 2014. Proceedings / / edited by Juergen Dingel, Wolfram Schulte, Isidro Ramos, Silvia Abrahao, Emilio Insfran
| Model-Driven Engineering Languages and Systems : 17th International Conference, MODELS 2014, Valencia, Spain, September 283– October 4, 2014. Proceedings / / edited by Juergen Dingel, Wolfram Schulte, Isidro Ramos, Silvia Abrahao, Emilio Insfran |
| Edizione | [1st ed. 2014.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2014 |
| Descrizione fisica | 1 online resource (XXVIII, 688 p. 227 illus.) |
| Disciplina | 005.1 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Programming languages (Electronic computers)
Software engineering Computer logic Management information systems Computer science Computer simulation Computer system failures Programming Languages, Compilers, Interpreters Software Engineering Logics and Meanings of Programs Management of Computing and Information Systems Simulation and Modeling System Performance and Evaluation |
| ISBN | 3-319-11653-3 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Cloud, Mobile and Web Computing -- Model-Driven Development of Mobile Applications Allowing Role-Driven Variants -- A Model-Based System to Automate Cloud Resource Allocation and Optimization -- An Evaluation of the Effectiveness of the Atomic Section Model -- Model Transformation 1 -- Parsing in a Broad Sense -- Streaming Model Transformations by Complex Event Processing -- On the Use of Signatures for Source Incremental Model-to-text Transformation -- Behavioral Modeling -- Modeling Systemic Behavior by State-Based Holonic Modular Units -- Semantic Model Differencing Utilizing Behavioral Semantics Specifications -- Formalizing Execution Semantics of UML Profiles with fUML Models -- MDE: Past, Present and Future.-Who Knows/Uses What of the UML: A Personal Opinion Survey -- Assessing the State-of-Practice of Model-Based Engineering in the Embedded Systems Domain -- The Relevance of Model-Driven Engineering Thirty Years from Now -- Formal Semantics, Specification and Verification -- Verifying Compilation of Synchronous Distributed Applications -- Environment-Centric Contracts for Design of Cyber-Physical Systems -- Removing Redundancies and Deducing Equivalences in UML Class Diagrams -- Models at Runtime -- A Native Versioning Concept to Support Historized Models at Runtime -- Modelling Adaptation Policies as Domain-Specific Constraints -- Scalable Armies of Model Clones through Data Sharing -- Feature and Variability Modeling -- Three Cases of Feature-Based Variability Modeling in Industry -- Supporting Multiplicity and Hierarchy in Model-Based Configuration: Experiences and Lessons Learned -- Propagating Decisions to Detect and Explain Conflicts in a Multi-step Configuration Process -- Composition and Adaptation -- An MDA Approach for the Generation of Communication Adapters Integrating SW and FW Components from Simulink -- A UML Model-Driven Approach to Efficiently Allocate Complex Communication Schemes -- Model-Integrating Software Components -- Practices and Experience -- Experiences in Applying Model Driven Engineering to the Telescope and Instrument Control System Domain -- Model Driven Grant Proposal Engineering -- Agile Model-Driven Engineering in Mechatronic Systems - An Industrial Case Study -- Modeling for Analysis -- Using UML for Modeling Procedural Legal Rules: Approach and a Study of Luxembourg’s Tax Law -- Resolution of Interfering Product Fragments in Software Product Line Engineering -- Ontology-Based Modeling of Context-Aware Systems -- Pragmatics -- Comprehending Feature Models Expressed in CVL -- On the Impact of Layout Quality to Understanding UML Diagrams: Size Matters -- Enabling the Development of Cognitive Effective Visual DSLs -- Model Extraction, Manipulation and Persistence -- JUMP—From Java Annotations to UML Profiles -- SIGMA: Scala Internal Domain-Specific Languages for Model Manipulations -- A Framework to Benchmark NoSQL Data Stores for Large-Scale Model Persistence -- Model Transformation 2 -- Automated Chaining of Model Transformations with Incompatible Metamodels -- Classification of Model Transformation Tools: Pattern Matching Techniques -- Learning Implicit and Explicit Control in Model Transformations by Example -- Querying and Reasoning IncQuery-D: A Distributed Incremental Model Query Framework in the Cloud -- Translating OCL to Graph Patterns. |
| Record Nr. | UNINA-9910484700503321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2014 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||