Software Technologies: Applications and Foundations [[electronic resource] ] : STAF 2017 Collocated Workshops, Marburg, Germany, July 17-21, 2017, Revised Selected Papers / / edited by Martina Seidl, Steffen Zschaler |
Edizione | [1st ed. 2018.] |
Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018 |
Descrizione fisica | 1 online resource (XXIV, 418 p. 133 illus.) |
Disciplina | 004 |
Collana | Programming and Software Engineering |
Soggetto topico |
Software engineering
Programming languages (Electronic computers) Computer programming Artificial intelligence Special purpose computers User interfaces (Computer systems) Software Engineering Programming Languages, Compilers, Interpreters Programming Techniques Artificial Intelligence Special Purpose and Application-Based Systems User Interfaces and Human Computer Interaction |
ISBN | 3-319-74730-4 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto |
Intro -- Preface -- STAF 2017 Organizer's Message -- BigMDE 2017 Organizers' Message -- GCM 2017 Organizers' Message -- GRAND 2017 Organizers' Message -- MORSE 2017 Organizers' Message -- OCL 2017 Organizers' Message -- Projects Showcase 2017 Organizers' Message -- Contents -- Scalable Model Driven Engineering (BigMDE) -- Injecting Execution Traces into a Model-Driven Framework for Program Analysis -- 1 Introduction -- 2 Approach -- 2.1 Model Driven Reverse Engineering -- 2.2 Model Transformation -- 2.3 Code Instrumentation -- 2.4 Execution and Completion -- 3 Evaluation -- 3.1 Execution Environment -- 3.2 Discussion -- 4 Related Work -- 5 Conclusion and Future Works -- References -- Introduction of an OpenCL-Based Model Transformation Engine -- 1 Introduction -- 2 Related Work -- 3 Parallel Multiplatform Model-Transformation Engine -- 3.1 The Representation of the Domain Model -- 3.2 Steps of the Approach -- 3.3 Illustrating the Topological Match -- 4 Conclusion and Future Work -- References -- Collaborative Modelling with Version Control -- Abstract -- 1 Introduction -- 2 Background and Related Research -- 2.1 Two Ways to Collaborate -- 2.2 Research on the "Clone and Merge" Approach -- 2.3 Research on the "Share and Lock" Approach -- 3 Current State of the Art -- 3.1 Clone and Merge: EMF Compare + EGit -- 3.2 Share and Lock: MetaEdit+ -- 4 Comparison Functionality in a Modelling Tool -- 4.1 View Changes as a Tree -- 4.2 Graphical Comparison to Highlight Changes -- 4.3 Textual Comparison with Model Links -- 5 Version Control System Integration -- 5.1 What to Version and How -- 6 Conclusions -- Acknowledgments -- References -- A Java Bytecode Metamodel for Composable Program Analyses -- 1 Introduction -- 2 Motivation -- 2.1 Motivating Example -- 2.2 Implementing Program Analyses with a Bytecode Toolkit -- 2.3 Composing the Toolkit-Based Analyses.
2.4 Problem Statement -- 3 Java Bytecode Metamodel -- 3.1 Structure of Java Bytecode Metamodel -- 3.2 JBCPP Plug-in -- 4 Related Work -- 5 Conclusion -- References -- Graph Computation Models (GCM) -- Graph Rewriting Based Search for Molecular Structures: Definitions, Algorithms, Hardness -- 1 Introduction -- 2 Definitions and Summary of the Results -- 3 Related Work -- 4 Normal Form of the Rules -- 5 An Algorithm for the Subgraph Matching -- 5.1 An Exponential Algorithm -- 5.2 Reducing the Number of Considered Subsets -- 6 NP-completeness for Rules of Unbounded Degree on Stars -- 7 W[1]-Hardness in the Degree for Trees -- 8 Estimating the Size of the DP-Table in a Large Database -- 9 Conclusion -- References -- Towards Automatic Generation of Evolution Rules for Model-Driven Optimisation -- 1 Introduction -- 2 Related Work -- 3 Running Example -- 4 Searching Optimal Models with Generated Rules -- 4.1 Specifying the Optimisation Problem -- 4.2 Generating the Rules -- 4.3 Running the Optimisation -- 5 Evaluation -- 6 Conclusions and Outlook -- References -- Generating Efficient Predictive Shift-Reduce Parsers for Hyperedge Replacement Grammars -- 1 Introduction -- 2 Hyperedge Replacement Grammars -- 3 Predictive Shift-Reduce Parsing for HR Grammars -- 4 Conflict Analysis -- 5 Efficient Implementation of PSR Parsers -- 6 Evaluation of Generated PSR Parsers -- 7 Conclusions -- References -- Checking Graph Programs for Confluence -- 1 Introduction -- 2 Graphs and Graph Programs -- 3 Symbolic Critical Pairs -- 4 Symbolic Rewriting and Joinability -- 4.1 Symbolic Rewriting -- 4.2 Joinability -- 5 Case Study: Shortest Distances -- 6 Local Confluence -- 7 Conclusion -- References -- Loose Graph Simulations -- 1 Introduction -- 2 Hosts, Guests and Loose Graph Simulations -- 3 An Algebra for Guests -- 4 The LGS Problem is NP-complete. 4.1 NP-Hardness: Subgraph Isomorphisms via LGSs -- 5 Graph Simulations Are Loose Graph Simulations -- 6 Regular Languages Pattern Matching -- 7 Subgraph Isomorphism with Regular Path Expressions -- 8 A Polynomial Fragment of LGSs -- 9 Conclusions and Future Work -- References -- Grand Challenges in Modeling (GRAND) -- Models, More Models, and Then a Lot More -- 1 Introduction -- 2 The Expanding Universe of MDE -- 3 Treating MDE Artefacts as Data -- 4 Relevant Domains for Model Analytics -- 5 Conclusion -- References -- On the Need for Temporal Model Repositories -- 1 Introduction -- 1.1 Why Temporal Model Repositories are Needed -- 1.2 Existing Work on Temporal Artifacts -- 1.3 Structure of this Paper -- 2 Motivating Example -- 3 Temporal Model Repositories Challenges -- 3.1 Model Storage -- 3.2 Model Consistency -- 3.3 Model Access -- 3.4 Model Manipulation -- 3.5 Model Visualization -- 3.6 Further Challenges -- 4 Conclusions -- References -- On the Need for Artifact Models in Model-Driven Systems Engineering Projects -- 1 Motivation -- 2 Modeling Artifact Relations -- 3 Example -- 4 State of the Art -- 5 Challenges of Artifact Modeling -- 6 Conclusion -- References -- Cognifying Model-Driven Software Engineering -- 1 Introduction -- 2 Opportunities in the Cognification of MDSE -- 2.1 Modeling Bots -- 2.2 Model Inferencers -- 2.3 Smart Code Generators -- 2.4 Real-Time Model Reviewers -- 2.5 Advanced Self-morphing and Collaborative Modeling Tools -- 2.6 Semantic Reasoning Platforms, Explainability and Storification -- 2.7 Scalable Model and Data Fusion Engine -- 3 Model-Driven Engineering of AI and Knowledge-Aware Software -- 4 Conclusions and Challenges -- References -- Non-human Modelers: Challenges and Roadmap for Reusable Self-explanation -- 1 Introduction -- 2 Discussed Topics -- 3 Background for Reusable Self-explanation -- 3.1 Traceability. 3.2 Model Versioning -- 3.3 Provenance -- 4 Example Scenario -- 4.1 Scenario Description -- 4.2 Approach for Reusable Self-explanation -- 5 Research Roadmap -- 6 Conclusion -- References -- Some Narrow and Broad Challenges in MDD -- 1 Introduction -- 2 Challenges for Model and Transformation Properties -- 3 Challenges for the Development Process -- 4 Conclusion -- References -- Modelling by the People, for the People -- Abstract -- 1 Introduction -- 2 Developments in Developer Demographics -- 3 Libraries, Frameworks and Languages -- 4 Related Research -- 5 Conclusion -- References -- From Building Systems Right to Building Right Systems -- Abstract -- 1 Introduction -- 2 Overview of Proposed Approach -- 3 Research Agenda -- 4 Exemplars -- 4.1 Digital Manufacturing -- 4.2 Integrated Computational Materials Engineering (ICME) -- 4.3 Model Driven Organisation (MDO) -- 5 Summary -- References -- The Tool Generation Challenge for Executable Domain-Specific Modeling Languages -- 1 Introduction -- 2 The Vision of Automated Tool Development -- 3 Open Challenges Towards Tool Generation -- 4 Conclusion -- References -- Toward Product Lines of Mathematical Models for Software Model Management -- 1 Introduction: Why Product Lines -- 2 Background: Why Abstract Models and Declarative Semantics -- 2.1 ``And Suddenly the Tool Doesn't Do Something Expected, and It Is a Nightmare for Them'' -- 2.2 Modelling Culture and Teaching It -- 2.3 Completeness of Classifications/Design Spaces -- 3 Model Synchronization and Its Challenges -- 3.1 A Sketch of (Symmetric) Delta Lenses -- 3.2 Organizational Symmetry and Organized Delta Lenses -- 3.3 Four Technical Challenges -- 4 Conclusion: Grand Challenges -- References -- Model-Driven Robot Software Engineering (MORSE) -- Model-Driven Interaction Design for Social Robots -- 1 Introduction -- 2 Project Description. 3 Problem Description & Stakeholders -- 4 Future Work -- 5 Conclusion -- References -- Towards Integration of Context-Based and Scenario-Based Development -- 1 Introduction -- 2 Scenario-Based Programming with Live Sequence Charts -- 3 Context-Based Specifications -- 4 Context-Based Design in Native LSC -- 5 Towards Intuitive Organization of Context-Based Specifications -- 6 Research on New Language Idioms -- References -- (An Example for) Formally Modeling Robot Behavior with UML and OCL -- 1 Introduction -- 2 A UML and OCL Model for a Production Line with Robotized Arms -- 3 Related Work -- 4 Conclusions and Future Work -- References -- Synthesizing Executable PLC Code for Robots from Scenario-Based GR(1) Specifications -- 1 Introduction -- 2 Example -- 3 Scenario-Based Modeling -- 4 Controller Synthesis -- 4.1 Play-Out -- 4.2 Synthesis -- 5 Generating Executable Code -- 5.1 Pre-processing the Controller -- 5.2 Generating Structured Text -- 5.3 Extensions -- 6 Related Work -- 7 Conclusion -- References -- Evaluating a Graph Query Language for Human-Robot Interaction Data in Smart Environments -- 1 Introduction -- 2 Language Modeling -- 3 Workbench Evaluation -- 3.1 Study Design -- 3.2 Tasks -- 3.3 Participant Preconditions -- 3.4 Questionnaire -- 3.5 Expectations -- 4 Pilot Study Results -- 5 Discussion and Lessons Learned -- 6 Related Work -- 7 Conclusion and Outlook -- References -- A Simulation Framework to Analyze Knowledge Exchange Strategies in Distributed Self-adaptive Systems -- 1 Introduction -- 2 A Simulation Infrastructure for Knowledge Exchange Strategies -- 2.1 Siafu Simulator -- 2.2 Concepts -- 2.3 Measurements -- 2.4 Extensibility -- 3 Evaluation -- 3.1 Running Example -- 3.2 Time Measurement -- 3.3 Knowledge Exchange -- 3.4 Results -- 4 Related Work -- 5 Conclusion and Future Work -- References -- OCL and Textual Modeling (OCL). Workshop in OCL and Textual Modelling. |
Record Nr. | UNISA-996465487303316 |
Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018 | ||
![]() | ||
Lo trovi qui: Univ. di Salerno | ||
|
Software Technologies: Applications and Foundations : STAF 2017 Collocated Workshops, Marburg, Germany, July 17-21, 2017, Revised Selected Papers / / edited by Martina Seidl, Steffen Zschaler |
Edizione | [1st ed. 2018.] |
Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018 |
Descrizione fisica | 1 online resource (XXIV, 418 p. 133 illus.) |
Disciplina | 004 |
Collana | Programming and Software Engineering |
Soggetto topico |
Software engineering
Programming languages (Electronic computers) Computer programming Artificial intelligence Special purpose computers User interfaces (Computer systems) Software Engineering Programming Languages, Compilers, Interpreters Programming Techniques Artificial Intelligence Special Purpose and Application-Based Systems User Interfaces and Human Computer Interaction |
ISBN | 3-319-74730-4 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto |
Intro -- Preface -- STAF 2017 Organizer's Message -- BigMDE 2017 Organizers' Message -- GCM 2017 Organizers' Message -- GRAND 2017 Organizers' Message -- MORSE 2017 Organizers' Message -- OCL 2017 Organizers' Message -- Projects Showcase 2017 Organizers' Message -- Contents -- Scalable Model Driven Engineering (BigMDE) -- Injecting Execution Traces into a Model-Driven Framework for Program Analysis -- 1 Introduction -- 2 Approach -- 2.1 Model Driven Reverse Engineering -- 2.2 Model Transformation -- 2.3 Code Instrumentation -- 2.4 Execution and Completion -- 3 Evaluation -- 3.1 Execution Environment -- 3.2 Discussion -- 4 Related Work -- 5 Conclusion and Future Works -- References -- Introduction of an OpenCL-Based Model Transformation Engine -- 1 Introduction -- 2 Related Work -- 3 Parallel Multiplatform Model-Transformation Engine -- 3.1 The Representation of the Domain Model -- 3.2 Steps of the Approach -- 3.3 Illustrating the Topological Match -- 4 Conclusion and Future Work -- References -- Collaborative Modelling with Version Control -- Abstract -- 1 Introduction -- 2 Background and Related Research -- 2.1 Two Ways to Collaborate -- 2.2 Research on the "Clone and Merge" Approach -- 2.3 Research on the "Share and Lock" Approach -- 3 Current State of the Art -- 3.1 Clone and Merge: EMF Compare + EGit -- 3.2 Share and Lock: MetaEdit+ -- 4 Comparison Functionality in a Modelling Tool -- 4.1 View Changes as a Tree -- 4.2 Graphical Comparison to Highlight Changes -- 4.3 Textual Comparison with Model Links -- 5 Version Control System Integration -- 5.1 What to Version and How -- 6 Conclusions -- Acknowledgments -- References -- A Java Bytecode Metamodel for Composable Program Analyses -- 1 Introduction -- 2 Motivation -- 2.1 Motivating Example -- 2.2 Implementing Program Analyses with a Bytecode Toolkit -- 2.3 Composing the Toolkit-Based Analyses.
2.4 Problem Statement -- 3 Java Bytecode Metamodel -- 3.1 Structure of Java Bytecode Metamodel -- 3.2 JBCPP Plug-in -- 4 Related Work -- 5 Conclusion -- References -- Graph Computation Models (GCM) -- Graph Rewriting Based Search for Molecular Structures: Definitions, Algorithms, Hardness -- 1 Introduction -- 2 Definitions and Summary of the Results -- 3 Related Work -- 4 Normal Form of the Rules -- 5 An Algorithm for the Subgraph Matching -- 5.1 An Exponential Algorithm -- 5.2 Reducing the Number of Considered Subsets -- 6 NP-completeness for Rules of Unbounded Degree on Stars -- 7 W[1]-Hardness in the Degree for Trees -- 8 Estimating the Size of the DP-Table in a Large Database -- 9 Conclusion -- References -- Towards Automatic Generation of Evolution Rules for Model-Driven Optimisation -- 1 Introduction -- 2 Related Work -- 3 Running Example -- 4 Searching Optimal Models with Generated Rules -- 4.1 Specifying the Optimisation Problem -- 4.2 Generating the Rules -- 4.3 Running the Optimisation -- 5 Evaluation -- 6 Conclusions and Outlook -- References -- Generating Efficient Predictive Shift-Reduce Parsers for Hyperedge Replacement Grammars -- 1 Introduction -- 2 Hyperedge Replacement Grammars -- 3 Predictive Shift-Reduce Parsing for HR Grammars -- 4 Conflict Analysis -- 5 Efficient Implementation of PSR Parsers -- 6 Evaluation of Generated PSR Parsers -- 7 Conclusions -- References -- Checking Graph Programs for Confluence -- 1 Introduction -- 2 Graphs and Graph Programs -- 3 Symbolic Critical Pairs -- 4 Symbolic Rewriting and Joinability -- 4.1 Symbolic Rewriting -- 4.2 Joinability -- 5 Case Study: Shortest Distances -- 6 Local Confluence -- 7 Conclusion -- References -- Loose Graph Simulations -- 1 Introduction -- 2 Hosts, Guests and Loose Graph Simulations -- 3 An Algebra for Guests -- 4 The LGS Problem is NP-complete. 4.1 NP-Hardness: Subgraph Isomorphisms via LGSs -- 5 Graph Simulations Are Loose Graph Simulations -- 6 Regular Languages Pattern Matching -- 7 Subgraph Isomorphism with Regular Path Expressions -- 8 A Polynomial Fragment of LGSs -- 9 Conclusions and Future Work -- References -- Grand Challenges in Modeling (GRAND) -- Models, More Models, and Then a Lot More -- 1 Introduction -- 2 The Expanding Universe of MDE -- 3 Treating MDE Artefacts as Data -- 4 Relevant Domains for Model Analytics -- 5 Conclusion -- References -- On the Need for Temporal Model Repositories -- 1 Introduction -- 1.1 Why Temporal Model Repositories are Needed -- 1.2 Existing Work on Temporal Artifacts -- 1.3 Structure of this Paper -- 2 Motivating Example -- 3 Temporal Model Repositories Challenges -- 3.1 Model Storage -- 3.2 Model Consistency -- 3.3 Model Access -- 3.4 Model Manipulation -- 3.5 Model Visualization -- 3.6 Further Challenges -- 4 Conclusions -- References -- On the Need for Artifact Models in Model-Driven Systems Engineering Projects -- 1 Motivation -- 2 Modeling Artifact Relations -- 3 Example -- 4 State of the Art -- 5 Challenges of Artifact Modeling -- 6 Conclusion -- References -- Cognifying Model-Driven Software Engineering -- 1 Introduction -- 2 Opportunities in the Cognification of MDSE -- 2.1 Modeling Bots -- 2.2 Model Inferencers -- 2.3 Smart Code Generators -- 2.4 Real-Time Model Reviewers -- 2.5 Advanced Self-morphing and Collaborative Modeling Tools -- 2.6 Semantic Reasoning Platforms, Explainability and Storification -- 2.7 Scalable Model and Data Fusion Engine -- 3 Model-Driven Engineering of AI and Knowledge-Aware Software -- 4 Conclusions and Challenges -- References -- Non-human Modelers: Challenges and Roadmap for Reusable Self-explanation -- 1 Introduction -- 2 Discussed Topics -- 3 Background for Reusable Self-explanation -- 3.1 Traceability. 3.2 Model Versioning -- 3.3 Provenance -- 4 Example Scenario -- 4.1 Scenario Description -- 4.2 Approach for Reusable Self-explanation -- 5 Research Roadmap -- 6 Conclusion -- References -- Some Narrow and Broad Challenges in MDD -- 1 Introduction -- 2 Challenges for Model and Transformation Properties -- 3 Challenges for the Development Process -- 4 Conclusion -- References -- Modelling by the People, for the People -- Abstract -- 1 Introduction -- 2 Developments in Developer Demographics -- 3 Libraries, Frameworks and Languages -- 4 Related Research -- 5 Conclusion -- References -- From Building Systems Right to Building Right Systems -- Abstract -- 1 Introduction -- 2 Overview of Proposed Approach -- 3 Research Agenda -- 4 Exemplars -- 4.1 Digital Manufacturing -- 4.2 Integrated Computational Materials Engineering (ICME) -- 4.3 Model Driven Organisation (MDO) -- 5 Summary -- References -- The Tool Generation Challenge for Executable Domain-Specific Modeling Languages -- 1 Introduction -- 2 The Vision of Automated Tool Development -- 3 Open Challenges Towards Tool Generation -- 4 Conclusion -- References -- Toward Product Lines of Mathematical Models for Software Model Management -- 1 Introduction: Why Product Lines -- 2 Background: Why Abstract Models and Declarative Semantics -- 2.1 ``And Suddenly the Tool Doesn't Do Something Expected, and It Is a Nightmare for Them'' -- 2.2 Modelling Culture and Teaching It -- 2.3 Completeness of Classifications/Design Spaces -- 3 Model Synchronization and Its Challenges -- 3.1 A Sketch of (Symmetric) Delta Lenses -- 3.2 Organizational Symmetry and Organized Delta Lenses -- 3.3 Four Technical Challenges -- 4 Conclusion: Grand Challenges -- References -- Model-Driven Robot Software Engineering (MORSE) -- Model-Driven Interaction Design for Social Robots -- 1 Introduction -- 2 Project Description. 3 Problem Description & Stakeholders -- 4 Future Work -- 5 Conclusion -- References -- Towards Integration of Context-Based and Scenario-Based Development -- 1 Introduction -- 2 Scenario-Based Programming with Live Sequence Charts -- 3 Context-Based Specifications -- 4 Context-Based Design in Native LSC -- 5 Towards Intuitive Organization of Context-Based Specifications -- 6 Research on New Language Idioms -- References -- (An Example for) Formally Modeling Robot Behavior with UML and OCL -- 1 Introduction -- 2 A UML and OCL Model for a Production Line with Robotized Arms -- 3 Related Work -- 4 Conclusions and Future Work -- References -- Synthesizing Executable PLC Code for Robots from Scenario-Based GR(1) Specifications -- 1 Introduction -- 2 Example -- 3 Scenario-Based Modeling -- 4 Controller Synthesis -- 4.1 Play-Out -- 4.2 Synthesis -- 5 Generating Executable Code -- 5.1 Pre-processing the Controller -- 5.2 Generating Structured Text -- 5.3 Extensions -- 6 Related Work -- 7 Conclusion -- References -- Evaluating a Graph Query Language for Human-Robot Interaction Data in Smart Environments -- 1 Introduction -- 2 Language Modeling -- 3 Workbench Evaluation -- 3.1 Study Design -- 3.2 Tasks -- 3.3 Participant Preconditions -- 3.4 Questionnaire -- 3.5 Expectations -- 4 Pilot Study Results -- 5 Discussion and Lessons Learned -- 6 Related Work -- 7 Conclusion and Outlook -- References -- A Simulation Framework to Analyze Knowledge Exchange Strategies in Distributed Self-adaptive Systems -- 1 Introduction -- 2 A Simulation Infrastructure for Knowledge Exchange Strategies -- 2.1 Siafu Simulator -- 2.2 Concepts -- 2.3 Measurements -- 2.4 Extensibility -- 3 Evaluation -- 3.1 Running Example -- 3.2 Time Measurement -- 3.3 Knowledge Exchange -- 3.4 Results -- 4 Related Work -- 5 Conclusion and Future Work -- References -- OCL and Textual Modeling (OCL). Workshop in OCL and Textual Modelling. |
Record Nr. | UNINA-9910349261403321 |
Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018 | ||
![]() | ||
Lo trovi qui: Univ. Federico II | ||
|
Tests and Proofs [[electronic resource] ] : 8th International Conference, TAP 2014, Held as Part of STAF 2014, York, UK, July 24-25, 2014, Proceedings / / edited by Martina Seidl, Nikolai Tillmann |
Edizione | [1st ed. 2014.] |
Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2014 |
Descrizione fisica | 1 online resource (XII, 214 p. 76 illus.) |
Disciplina | 004 |
Collana | Programming and Software Engineering |
Soggetto topico |
Software engineering
Computer programming Computer logic Mathematical logic Programming languages (Electronic computers) Computer simulation Software Engineering Programming Techniques Logics and Meanings of Programs Mathematical Logic and Formal Languages Programming Languages, Compilers, Interpreters Simulation and Modeling |
ISBN | 3-319-09099-2 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Model-Based Mutation Testing of an Industrial Measurement Device -- Computing with an SMT Solver -- An Abstraction Technique for Testing Decomposable Systems by Model Checking -- An All-in-One Toolkit for Automated White-Box Testing -- Behaviour Driven Development for Tests and Verification -- Quality Assurance in MBE Back and Forth -- Visualizing Unbounded Symbolic Execution -- Film stripping and Unrolling: A Comparison of Verification Approaches for UML and OCL Behavioral Models -- Generating Classified Parallel Unit Tests -- JTACO: Test Execution for Faster Bounded Verification -- Explicit Assumptions - A Prenup for Marrying Static and Dynamic Program Verification -- A Case Study on Verification of a Cloud Hypervisor by Proof and Structural Testing -- Runtime Assertion Checking and Its Combinations with Static and Dynamic Analyses: Tutorial Synopsis -- Generating Test Data from a UML Activity Using the AMPL Interface for Constraint Solvers -- Lightweight State Capturing for Automated Testing of Multithreaded Programs -- How Test Generation Helps Software Specification and Deductive Verification in Frama-C. |
Record Nr. | UNISA-996213834703316 |
Cham : , : Springer International Publishing : , : Imprint : Springer, , 2014 | ||
![]() | ||
Lo trovi qui: Univ. di Salerno | ||
|
Tests and Proofs : 8th International Conference, TAP 2014, Held as Part of STAF 2014, York, UK, July 24-25, 2014, Proceedings / / edited by Martina Seidl, Nikolai Tillmann |
Edizione | [1st ed. 2014.] |
Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2014 |
Descrizione fisica | 1 online resource (XII, 214 p. 76 illus.) |
Disciplina | 004 |
Collana | Programming and Software Engineering |
Soggetto topico |
Software engineering
Computer programming Computer logic Mathematical logic Programming languages (Electronic computers) Computer simulation Software Engineering Programming Techniques Logics and Meanings of Programs Mathematical Logic and Formal Languages Programming Languages, Compilers, Interpreters Simulation and Modeling |
ISBN | 3-319-09099-2 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Model-Based Mutation Testing of an Industrial Measurement Device -- Computing with an SMT Solver -- An Abstraction Technique for Testing Decomposable Systems by Model Checking -- An All-in-One Toolkit for Automated White-Box Testing -- Behaviour Driven Development for Tests and Verification -- Quality Assurance in MBE Back and Forth -- Visualizing Unbounded Symbolic Execution -- Film stripping and Unrolling: A Comparison of Verification Approaches for UML and OCL Behavioral Models -- Generating Classified Parallel Unit Tests -- JTACO: Test Execution for Faster Bounded Verification -- Explicit Assumptions - A Prenup for Marrying Static and Dynamic Program Verification -- A Case Study on Verification of a Cloud Hypervisor by Proof and Structural Testing -- Runtime Assertion Checking and Its Combinations with Static and Dynamic Analyses: Tutorial Synopsis -- Generating Test Data from a UML Activity Using the AMPL Interface for Constraint Solvers -- Lightweight State Capturing for Automated Testing of Multithreaded Programs -- How Test Generation Helps Software Specification and Deductive Verification in Frama-C. |
Record Nr. | UNINA-9910484698003321 |
Cham : , : Springer International Publishing : , : Imprint : Springer, , 2014 | ||
![]() | ||
Lo trovi qui: Univ. Federico II | ||
|
Theory and Applications of Satisfiability Testing – SAT 2020 [[electronic resource] ] : 23rd International Conference, Alghero, Italy, July 3–10, 2020, Proceedings / / edited by Luca Pulina, Martina Seidl |
Edizione | [1st ed. 2020.] |
Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2020 |
Descrizione fisica | 1 online resource (xi, 538 pages) |
Disciplina | 005.1 |
Collana | Theoretical Computer Science and General Issues |
Soggetto topico |
Computer science
Computer engineering Computer networks Microprogramming Numerical analysis Logic programming Software engineering Theory of Computation Computer Engineering and Networks Control Structures and Microprogramming Numerical Analysis Logic in AI Software Engineering |
ISBN | 3-030-51825-6 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Sorting Parity Encodings by Reusing Variables -- Community and LBD-based Clause Sharing Policy for Parallel SAT Solving -- Clause size reduction with all-UIP Learning -- Trail Saving on Backtrack -- Four Flavors of Entailment -- Designing New Phase Selection Heuristics -- On the Effect of Learned Clauses on Stochastic Local Search -- SAT Heritage: a community-driven effort for archiving, building and running more than thousand SAT solvers -- Distributed Cube and Conquer with Paracooba -- Reproducible E cient Parallel SAT Solving -- Improving Implementation of SAT Competitions 2017-2019 Winners -- On CDCL-based Proof Systems with the Ordered Decision Strategy -- Equivalence Between Systems Stronger Than Resolution -- Simplified and Improved Separations Between Regular and General Resolution by Lifting -- Mycielski graphs and PR proofs -- Towards a Better Understanding of (Partial Weighted) MaxSAT Proof Systems -- Towards a Complexity-theoretic Understanding of Restarts in SAT solvers -- On the Sparsity of XORs in Approximate Model Counting -- A Faster Algorithm for Propositional Model Counting Parameterized by Incidence Treewidth -- Abstract Cores in Implicit Hitting Set MaxSat Solving -- MaxSAT Resolution and SubCube Sums -- A Lower Bound on DNNF Encodings of Pseudo-Boolean Constraints -- On Weakening Strategies for PB Solvers -- Reasoning About Strong Inconsistency in ASP -- Taming High Treewidth with Abstraction, Nested Dynamic Programming, and Database Technology -- Reducing Bit-Vector Polynomials to SAT using Groebner Bases -- Speeding Up Quantified Bit-Vector SMT Solvers by Bit-Width Reductions and Extensions -- Strong (D)QBF Dependency Schemes via Tautology-free Resolution Paths -- Short Q-Resolution Proofs with Homomorphisms -- Multi-Linear Strategy Extraction for QBF Expansion Proofs via Local Soundness -- Positional Games and QBF: The Corrective Encoding -- Matrix Multiplication: Verifying Strong Uniquely Solvable Puzzles -- Satisfiability Solving Meets Evolutionary Optimisation in Designing Approximate Circuits -- SAT Solving with Fragmented Hamiltonian Path Constraints for Wire Arc Additive Manufacturing -- SAT-based Encodings for Optimal Decision Trees with Explicit Paths -- Incremental Encoding of Pseudo-Boolean Goal Functions based on Comparator Networks. . |
Record Nr. | UNISA-996418280803316 |
Cham : , : Springer International Publishing : , : Imprint : Springer, , 2020 | ||
![]() | ||
Lo trovi qui: Univ. di Salerno | ||
|
Theory and Applications of Satisfiability Testing – SAT 2020 : 23rd International Conference, Alghero, Italy, July 3–10, 2020, Proceedings / / edited by Luca Pulina, Martina Seidl |
Edizione | [1st ed. 2020.] |
Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2020 |
Descrizione fisica | 1 online resource (xi, 538 pages) |
Disciplina | 005.1 |
Collana | Theoretical Computer Science and General Issues |
Soggetto topico |
Computer science
Computer engineering Computer networks Microprogramming Numerical analysis Logic programming Software engineering Theory of Computation Computer Engineering and Networks Control Structures and Microprogramming Numerical Analysis Logic in AI Software Engineering |
ISBN | 3-030-51825-6 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Sorting Parity Encodings by Reusing Variables -- Community and LBD-based Clause Sharing Policy for Parallel SAT Solving -- Clause size reduction with all-UIP Learning -- Trail Saving on Backtrack -- Four Flavors of Entailment -- Designing New Phase Selection Heuristics -- On the Effect of Learned Clauses on Stochastic Local Search -- SAT Heritage: a community-driven effort for archiving, building and running more than thousand SAT solvers -- Distributed Cube and Conquer with Paracooba -- Reproducible E cient Parallel SAT Solving -- Improving Implementation of SAT Competitions 2017-2019 Winners -- On CDCL-based Proof Systems with the Ordered Decision Strategy -- Equivalence Between Systems Stronger Than Resolution -- Simplified and Improved Separations Between Regular and General Resolution by Lifting -- Mycielski graphs and PR proofs -- Towards a Better Understanding of (Partial Weighted) MaxSAT Proof Systems -- Towards a Complexity-theoretic Understanding of Restarts in SAT solvers -- On the Sparsity of XORs in Approximate Model Counting -- A Faster Algorithm for Propositional Model Counting Parameterized by Incidence Treewidth -- Abstract Cores in Implicit Hitting Set MaxSat Solving -- MaxSAT Resolution and SubCube Sums -- A Lower Bound on DNNF Encodings of Pseudo-Boolean Constraints -- On Weakening Strategies for PB Solvers -- Reasoning About Strong Inconsistency in ASP -- Taming High Treewidth with Abstraction, Nested Dynamic Programming, and Database Technology -- Reducing Bit-Vector Polynomials to SAT using Groebner Bases -- Speeding Up Quantified Bit-Vector SMT Solvers by Bit-Width Reductions and Extensions -- Strong (D)QBF Dependency Schemes via Tautology-free Resolution Paths -- Short Q-Resolution Proofs with Homomorphisms -- Multi-Linear Strategy Extraction for QBF Expansion Proofs via Local Soundness -- Positional Games and QBF: The Corrective Encoding -- Matrix Multiplication: Verifying Strong Uniquely Solvable Puzzles -- Satisfiability Solving Meets Evolutionary Optimisation in Designing Approximate Circuits -- SAT Solving with Fragmented Hamiltonian Path Constraints for Wire Arc Additive Manufacturing -- SAT-based Encodings for Optimal Decision Trees with Explicit Paths -- Incremental Encoding of Pseudo-Boolean Goal Functions based on Comparator Networks. . |
Record Nr. | UNINA-9910410060203321 |
Cham : , : Springer International Publishing : , : Imprint : Springer, , 2020 | ||
![]() | ||
Lo trovi qui: Univ. Federico II | ||
|