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.
Construction and Analysis of Safe, Secure, and Interoperable Smart Devices [[electronic resource] ] : Second International Workshop, CASSIS 2005, Nice, France, March 8-11, 2005, Revised Selected Papers / / edited by Gilles Barthe, Benjamin Gregoire, Marieke Huisman, Jean-Luis Lanet
| Construction and Analysis of Safe, Secure, and Interoperable Smart Devices [[electronic resource] ] : Second International Workshop, CASSIS 2005, Nice, France, March 8-11, 2005, Revised Selected Papers / / edited by Gilles Barthe, Benjamin Gregoire, Marieke Huisman, Jean-Luis Lanet |
| Edizione | [1st ed. 2006.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2006 |
| Descrizione fisica | 1 online resource (X, 173 p.) |
| Disciplina | 005.1 |
| Collana | Security and Cryptology |
| Soggetto topico |
Software engineering
Special purpose computers Computer programming Programming languages (Electronic computers) Operating systems (Computers) Computer logic Software Engineering Special Purpose and Application-Based Systems Programming Techniques Programming Languages, Compilers, Interpreters Operating Systems Logics and Meanings of Programs |
| ISBN | 3-540-33691-5 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | The Architecture of a Privacy-Aware Access Control Decision Component -- Mobile Resource Guarantees and Policies -- Information Flow Analysis for a Typed Assembly Language with Polymorphic Stacks -- Romization: Early Deployment and Customization of Java Systems for Constrained Devices -- Typed Compilation Against Non-manifest Base Classes -- The Design of Application-Tailorable Operating System Product Lines -- Bringing Ease and Adaptability to MPSoC Software Design: A Component-Based Approach -- Modular Proof Principles for Parameterised Concretizations -- Formalisation and Verification of the GlobalPlatform Card Specification Using the B Method. |
| Record Nr. | UNISA-996466163403316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2006 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Construction and Analysis of Safe, Secure, and Interoperable Smart Devices [[electronic resource] ] : International Workshop, CASSIS 2004, Marseille, France, March 10-14, 2004, Revised Selected Papers / / edited by Gilles Barthe, Lilian Burdy, Marieke Huisman, Jean-Louis Lanet, Traian Muntean
| Construction and Analysis of Safe, Secure, and Interoperable Smart Devices [[electronic resource] ] : International Workshop, CASSIS 2004, Marseille, France, March 10-14, 2004, Revised Selected Papers / / edited by Gilles Barthe, Lilian Burdy, Marieke Huisman, Jean-Louis Lanet, Traian Muntean |
| Edizione | [1st ed. 2005.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2005 |
| Descrizione fisica | 1 online resource (IX, 258 p.) |
| Disciplina | 332.1/78 |
| Collana | Security and Cryptology |
| Soggetto topico |
Data encryption (Computer science)
Software engineering Special purpose computers Computer programming Programming languages (Electronic computers) Operating systems (Computers) Cryptology Software Engineering Special Purpose and Application-Based Systems Programming Techniques Programming Languages, Compilers, Interpreters Operating Systems |
| ISBN | 3-540-30569-6 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Mobile Resource Guarantees for Smart Devices -- History-Based Access Control and Secure Information Flow -- The Spec# Programming System: An Overview -- Mastering Test Generation from Smart Card Software Formal Models -- A Mechanism for Secure, Fine-Grained Dynamic Provisioning of Applications on Small Devices -- ESC/Java2: Uniting ESC/Java and JML -- A Type System for Checking Applet Isolation in Java Card -- Verification of Safety Properties in the Presence of Transactions -- Modelling Mobility Aspects of Security Policies -- Smart Devices for Next Generation Mobile Services -- A Flexible Framework for the Estimation of Coverage Metrics in Explicit State Software Model Checking -- Combining Several Paradigms for Circuit Validation and Verification -- Smart Card Research Perspectives. |
| Record Nr. | UNISA-996466053503316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2005 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Formal methods : 24th International Symposium, FM 2021, Virtual event, November 20-26, 2021, Proceedings / / Marieke Huisman, Corina Păsăreanu, Naijun Zhan (editors)
| Formal methods : 24th International Symposium, FM 2021, Virtual event, November 20-26, 2021, Proceedings / / Marieke Huisman, Corina Păsăreanu, Naijun Zhan (editors) |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2021] |
| Descrizione fisica | 1 online resource (801 pages) |
| Disciplina | 004.0151 |
| Collana | Lecture notes in computer science |
| Soggetto topico | Formal methods (Computer science) |
| ISBN | 3-030-90870-4 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNINA-9910508438803321 |
| Cham, Switzerland : , : Springer, , [2021] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Formal methods : 24th International Symposium, FM 2021, Virtual event, November 20-26, 2021, Proceedings / / Marieke Huisman, Corina Păsăreanu, Naijun Zhan (editors)
| Formal methods : 24th International Symposium, FM 2021, Virtual event, November 20-26, 2021, Proceedings / / Marieke Huisman, Corina Păsăreanu, Naijun Zhan (editors) |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2021] |
| Descrizione fisica | 1 online resource (801 pages) |
| Disciplina | 004.0151 |
| Collana | Lecture notes in computer science |
| Soggetto topico | Formal methods (Computer science) |
| ISBN | 3-030-90870-4 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNISA-996464527203316 |
| Cham, Switzerland : , : Springer, , [2021] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Formal methods for industrial critical systems : 27th International Conference, FMICS 2022, Warsaw, Poland, September 14-15, 2022, proceedings / / Jan Friso Groote, Marieke Huisman (editors)
| Formal methods for industrial critical systems : 27th International Conference, FMICS 2022, Warsaw, Poland, September 14-15, 2022, proceedings / / Jan Friso Groote, Marieke Huisman (editors) |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2022] |
| Descrizione fisica | 1 online resource (246 pages) |
| Disciplina | 004.0151 |
| Collana | Lecture notes in computer science |
| Soggetto topico |
Formal methods (Computer science)
Software engineering |
| ISBN | 3-031-15008-2 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Preface -- Organization -- Contents -- Invited Keynote Talks -- Reinforcement Learning with Guarantees that Hold for Ever -- 1 Learning from Rewards -- 2 Learning with -Regular Objectives -- 2.1 Good-for-MDP Automata -- 2.2 From GFM Büchi Automata to Reachability and RL -- 3 Related Work -- References -- Supporting Railway Innovations with Formal Modelling and Verification -- References -- Certification -- Formal Monotony Analysis of Neural Networks with Mixed Inputs: An Asset for Certification -- 1 Introduction -- 2 Certification Preamble -- 3 Related Work -- 4 Monotony Analysis -- 4.1 Goal of the Analysis -- 4.2 MILP Formulation -- 4.3 Verification Procedure -- 5 Case Study: Braking Distance Estimation -- 5.1 Description of the Case Study -- 5.2 Experimentation -- 6 Conclusion -- References -- Generating Domain-Specific Interactive Validation Documents -- 1 Introduction and Motivation -- 2 Validation Workflow -- 3 Static VisB HTML Export -- 4 Dynamic HTML Export: Code Generation to HTML and JavaScript -- 4.1 Graphical User Interface -- 4.2 Applicability of JavaScript Code Generation -- 5 Case Studies -- 6 Related Work -- 7 Conclusion and Future Work -- References -- Deductive Verification of Smart Contracts with Dafny -- 1 Introduction -- 2 Verification of Closed Smart Contracts -- 3 Verification Under Adversarial Conditions -- 3.1 Aborting a Computation -- 3.2 Reasoning with Arbitrary External Calls -- 4 Conclusion -- References -- Industrial Use Cases -- Towards Reusable Formal Models for Custom Real-Time Operating Systems -- 1 Introduction -- 2 Preliminaries -- 2.1 Core Components of Real-Time Operating Systems -- 2.2 Uppaal Timed Automata -- 3 Related Work -- 4 Reusable Formal Models for Custom RTOS -- 4.1 Formalization of Tasks -- 4.2 Formalization of Cyclic Handlers -- 4.3 Events and Timing Behavior.
4.4 Configurable Formal Scheduler Model -- 4.5 Modeling Sensor Inputs and Communication -- 5 Case Study: Search and Rescue Robots -- 6 Conclusion -- References -- Formal Verification of an Industrial UML-like Model using mCRL2 -- 1 Introduction -- 2 Cordis Models -- 2.1 Class Diagrams -- 2.2 State Machine Diagrams -- 3 Cylinder -- 4 Model Checking Cordis Models Using mCRL2 -- 4.1 Translation to mCRL2 -- 4.2 Formal Verification of Requirements -- 4.3 Results -- 5 Discussion -- 6 Concluding Remarks -- References -- Chemical Case Studies in KeYmaera X -- 1 Introduction -- 2 Background -- 2.1 Differential Dynamic Logic -- 2.2 KeYmaera X -- 3 Results -- 3.1 Controlled Irreversible Reactions -- 3.2 Uncontrolled Reversible Reactions -- 4 Related Work -- 5 Conclusion -- References -- Analysing Capacity Bottlenecks in Rail Infrastructure by Episode Mining -- 1 Introduction -- 2 Related Work -- 3 Identification of Capacity Bottlenecks -- 3.1 Method -- 3.2 Results -- 4 Analysing Delay Propagations -- 4.1 Goals and Overview -- 4.2 Episode Mining -- 4.3 Algorithm and Implementation -- 4.4 Adaptations -- 5 Evaluation Results -- 6 Conclusions and Outlook -- References -- Testing and Monitoring -- Test Suite Augmentation for Reconfigurable PLC Software in the Internet of Production -- 1 Introduction -- 1.1 Limitations and Contributions -- 2 Related Work -- 3 Methodology -- 3.1 Intermediate Representation -- 3.2 Bounded Symbolic Execution -- 3.3 Shadow Symbolic Execution -- 4 Evaluation -- 5 Conclusion -- References -- Monitoring of Spatio-Temporal Properties with Nonlinear SAT Solvers -- 1 Introduction -- 2 Preliminaries -- 3 Running Example -- 3.1 Formalization of Road Traffic Rules with LTL MS -- 3.2 Scenario and Trace Encoding (Static and Dynamic Objects) -- 4 Monitoring Model Construction -- 5 Empirical Evaluation -- 6 Related Work. 7 Conclusion and Future Work -- References -- Model-Based Testing of Internet of Things Protocols -- 1 Introduction -- 1.1 Related Work -- 1.2 Contributions -- 2 Preliminaries -- 2.1 Internet of Things -- 2.2 Model-Based Testing -- 2.3 Axini Modeling Platform (AMP) -- 3 MBT in the Context of IoT -- 3.1 IoT Testing Challenges -- 3.2 Positioning MBT in IoT -- 4 The AMP MBT Environment to Test BLE IoT Systems -- 4.1 SUT -- 4.2 Model Creation -- 4.3 AML Model Example -- 4.4 Adapter -- 5 Testing BLE Using AMP -- 5.1 Assumption -- 5.2 Test Generation Configurations -- 5.3 Conformance Experiment -- 5.4 Model Assumption Experiment -- 6 Discussion -- 7 Conclusion -- 7.1 Future Work -- References -- Methodology -- Formally Verifying Decompositions of Stochastic Specifications -- 1 Introduction -- 2 Problem Illustration -- 3 A Theory for Specifying Stochastic Behavior -- 3.1 Traces and Behaviors -- 3.2 Specifications -- 3.3 Trace Automata -- 3.4 Probabilistic Automaton Contracts -- 4 Verification of Refinement -- 5 Case Study -- 6 Related Work -- 7 Conclusions -- References -- Verification of Behavior Trees using Linear Constrained Horn Clauses -- 1 Introduction -- 2 Related Works -- 3 Preliminaries -- 3.1 Behavior Trees -- 3.2 Constrained Horn Clauses -- 4 Encoding of Behavior Trees -- 4.1 Idea -- 4.2 Action Node -- 4.3 Condition Node -- 4.4 Sequence Node -- 4.5 Sequence Node with Memory -- 4.6 Selector Node -- 4.7 Parallel Node -- 4.8 Root Node -- 4.9 Safety Property -- 4.10 Environment -- 5 Experiments -- 5.1 Benchmark -- 5.2 Discussion -- 6 Conclusion and Outlook -- References -- A Multi-level Methodology for Behavioral Comparison of Software-Intensive Systems -- 1 Introduction -- 2 Background -- 2.1 Software Behavior -- 2.2 State Machines -- 2.3 State Machine Comparison -- 3 Behavioral Comparison Methodology -- 3.1 Level 1: Model Set Variants. 3.2 Level 2: Model Set Variant Relations -- 3.3 Level 3: Model Set Variant Differences -- 3.4 Level 4: Model Variants -- 3.5 Level 5: Model Variant Relations -- 3.6 Level 6: Model Variant Differences -- 4 Evaluation -- 4.1 Case Study 1: Legacy Component Technology Migration -- 4.2 Case Study 2: System Behavior Matching Recipe -- 5 Conclusions and Future Work -- References -- Author Index. |
| Record Nr. | UNINA-9910591039203321 |
| Cham, Switzerland : , : Springer, , [2022] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Formal methods for industrial critical systems : 27th International Conference, FMICS 2022, Warsaw, Poland, September 14-15, 2022, proceedings / / Jan Friso Groote, Marieke Huisman (editors)
| Formal methods for industrial critical systems : 27th International Conference, FMICS 2022, Warsaw, Poland, September 14-15, 2022, proceedings / / Jan Friso Groote, Marieke Huisman (editors) |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2022] |
| Descrizione fisica | 1 online resource (246 pages) |
| Disciplina | 004.0151 |
| Collana | Lecture notes in computer science |
| Soggetto topico |
Formal methods (Computer science)
Software engineering |
| ISBN | 3-031-15008-2 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Preface -- Organization -- Contents -- Invited Keynote Talks -- Reinforcement Learning with Guarantees that Hold for Ever -- 1 Learning from Rewards -- 2 Learning with -Regular Objectives -- 2.1 Good-for-MDP Automata -- 2.2 From GFM Büchi Automata to Reachability and RL -- 3 Related Work -- References -- Supporting Railway Innovations with Formal Modelling and Verification -- References -- Certification -- Formal Monotony Analysis of Neural Networks with Mixed Inputs: An Asset for Certification -- 1 Introduction -- 2 Certification Preamble -- 3 Related Work -- 4 Monotony Analysis -- 4.1 Goal of the Analysis -- 4.2 MILP Formulation -- 4.3 Verification Procedure -- 5 Case Study: Braking Distance Estimation -- 5.1 Description of the Case Study -- 5.2 Experimentation -- 6 Conclusion -- References -- Generating Domain-Specific Interactive Validation Documents -- 1 Introduction and Motivation -- 2 Validation Workflow -- 3 Static VisB HTML Export -- 4 Dynamic HTML Export: Code Generation to HTML and JavaScript -- 4.1 Graphical User Interface -- 4.2 Applicability of JavaScript Code Generation -- 5 Case Studies -- 6 Related Work -- 7 Conclusion and Future Work -- References -- Deductive Verification of Smart Contracts with Dafny -- 1 Introduction -- 2 Verification of Closed Smart Contracts -- 3 Verification Under Adversarial Conditions -- 3.1 Aborting a Computation -- 3.2 Reasoning with Arbitrary External Calls -- 4 Conclusion -- References -- Industrial Use Cases -- Towards Reusable Formal Models for Custom Real-Time Operating Systems -- 1 Introduction -- 2 Preliminaries -- 2.1 Core Components of Real-Time Operating Systems -- 2.2 Uppaal Timed Automata -- 3 Related Work -- 4 Reusable Formal Models for Custom RTOS -- 4.1 Formalization of Tasks -- 4.2 Formalization of Cyclic Handlers -- 4.3 Events and Timing Behavior.
4.4 Configurable Formal Scheduler Model -- 4.5 Modeling Sensor Inputs and Communication -- 5 Case Study: Search and Rescue Robots -- 6 Conclusion -- References -- Formal Verification of an Industrial UML-like Model using mCRL2 -- 1 Introduction -- 2 Cordis Models -- 2.1 Class Diagrams -- 2.2 State Machine Diagrams -- 3 Cylinder -- 4 Model Checking Cordis Models Using mCRL2 -- 4.1 Translation to mCRL2 -- 4.2 Formal Verification of Requirements -- 4.3 Results -- 5 Discussion -- 6 Concluding Remarks -- References -- Chemical Case Studies in KeYmaera X -- 1 Introduction -- 2 Background -- 2.1 Differential Dynamic Logic -- 2.2 KeYmaera X -- 3 Results -- 3.1 Controlled Irreversible Reactions -- 3.2 Uncontrolled Reversible Reactions -- 4 Related Work -- 5 Conclusion -- References -- Analysing Capacity Bottlenecks in Rail Infrastructure by Episode Mining -- 1 Introduction -- 2 Related Work -- 3 Identification of Capacity Bottlenecks -- 3.1 Method -- 3.2 Results -- 4 Analysing Delay Propagations -- 4.1 Goals and Overview -- 4.2 Episode Mining -- 4.3 Algorithm and Implementation -- 4.4 Adaptations -- 5 Evaluation Results -- 6 Conclusions and Outlook -- References -- Testing and Monitoring -- Test Suite Augmentation for Reconfigurable PLC Software in the Internet of Production -- 1 Introduction -- 1.1 Limitations and Contributions -- 2 Related Work -- 3 Methodology -- 3.1 Intermediate Representation -- 3.2 Bounded Symbolic Execution -- 3.3 Shadow Symbolic Execution -- 4 Evaluation -- 5 Conclusion -- References -- Monitoring of Spatio-Temporal Properties with Nonlinear SAT Solvers -- 1 Introduction -- 2 Preliminaries -- 3 Running Example -- 3.1 Formalization of Road Traffic Rules with LTL MS -- 3.2 Scenario and Trace Encoding (Static and Dynamic Objects) -- 4 Monitoring Model Construction -- 5 Empirical Evaluation -- 6 Related Work. 7 Conclusion and Future Work -- References -- Model-Based Testing of Internet of Things Protocols -- 1 Introduction -- 1.1 Related Work -- 1.2 Contributions -- 2 Preliminaries -- 2.1 Internet of Things -- 2.2 Model-Based Testing -- 2.3 Axini Modeling Platform (AMP) -- 3 MBT in the Context of IoT -- 3.1 IoT Testing Challenges -- 3.2 Positioning MBT in IoT -- 4 The AMP MBT Environment to Test BLE IoT Systems -- 4.1 SUT -- 4.2 Model Creation -- 4.3 AML Model Example -- 4.4 Adapter -- 5 Testing BLE Using AMP -- 5.1 Assumption -- 5.2 Test Generation Configurations -- 5.3 Conformance Experiment -- 5.4 Model Assumption Experiment -- 6 Discussion -- 7 Conclusion -- 7.1 Future Work -- References -- Methodology -- Formally Verifying Decompositions of Stochastic Specifications -- 1 Introduction -- 2 Problem Illustration -- 3 A Theory for Specifying Stochastic Behavior -- 3.1 Traces and Behaviors -- 3.2 Specifications -- 3.3 Trace Automata -- 3.4 Probabilistic Automaton Contracts -- 4 Verification of Refinement -- 5 Case Study -- 6 Related Work -- 7 Conclusions -- References -- Verification of Behavior Trees using Linear Constrained Horn Clauses -- 1 Introduction -- 2 Related Works -- 3 Preliminaries -- 3.1 Behavior Trees -- 3.2 Constrained Horn Clauses -- 4 Encoding of Behavior Trees -- 4.1 Idea -- 4.2 Action Node -- 4.3 Condition Node -- 4.4 Sequence Node -- 4.5 Sequence Node with Memory -- 4.6 Selector Node -- 4.7 Parallel Node -- 4.8 Root Node -- 4.9 Safety Property -- 4.10 Environment -- 5 Experiments -- 5.1 Benchmark -- 5.2 Discussion -- 6 Conclusion and Outlook -- References -- A Multi-level Methodology for Behavioral Comparison of Software-Intensive Systems -- 1 Introduction -- 2 Background -- 2.1 Software Behavior -- 2.2 State Machines -- 2.3 State Machine Comparison -- 3 Behavioral Comparison Methodology -- 3.1 Level 1: Model Set Variants. 3.2 Level 2: Model Set Variant Relations -- 3.3 Level 3: Model Set Variant Differences -- 3.4 Level 4: Model Variants -- 3.5 Level 5: Model Variant Relations -- 3.6 Level 6: Model Variant Differences -- 4 Evaluation -- 4.1 Case Study 1: Legacy Component Technology Migration -- 4.2 Case Study 2: System Behavior Matching Recipe -- 5 Conclusions and Future Work -- References -- Author Index. |
| Record Nr. | UNISA-996490368003316 |
| Cham, Switzerland : , : Springer, , [2022] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Fundamental Approaches to Software Engineering [[electronic resource] ] : 20th International Conference, FASE 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings / / edited by Marieke Huisman, Julia Rubin
| Fundamental Approaches to Software Engineering [[electronic resource] ] : 20th International Conference, FASE 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings / / edited by Marieke Huisman, Julia Rubin |
| Edizione | [1st ed. 2017.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2017 |
| Descrizione fisica | 1 online resource (XIII, 444 p. 130 illus.) |
| Disciplina | 005.1 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Software engineering
Compilers (Computer programs) Computer science Machine theory Software Engineering Compilers and Interpreters Computer Science Logic and Foundations of Programming Formal Languages and Automata Theory |
| ISBN | 3-662-54494-6 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Learning and Inference -- Should We Learn Probabilistic Models for Model Checking? A New Approach and an Empirical Study -- Bordeaux: a tool for thinking outside the box -- Test Selection -- Bucketing Failing Tests via Symbolic Analysis -- Selective Bisection Debugging. - On the Effectiveness of Bug Predictors with Procedural Systems: a Quantitative Study -- Program and System Analysis -- Inference and Evolution of TypeScript Declaration Files -- Explicit Connection Actions in Multiparty Session Types -- Change and Delay Contracts for Hybrid System Component Verification. - Precise Version Control of Trees with Line-based Version Control Systems -- Graph Modelling and Transformation -- StaticGen: Static Generation of UML Sequence Diagrams -- Inter-Model Consistency Checking using Triple Graph Grammars and Linear Optimization Techniques -- GTS Families for the Flexible Composition of Graph Transformation Systems -- Symbolic Model Generation for Graph Properties. - Model Transformations -- Traceability Mappings as a Fundamental Instrument in Model Transformations -- Reusing Model Transformations through Typing Requirement Models -- Change-preserving model repair. -A deductive approach for fault localization in ATL model transformations. -Configuration and Synthesis -- OpenSAW: Open Security Analysis Workbench -- Visual Configuration of Mobile Privacy Policies -- Automated Workarounds from Java Program Specifications based on SAT Solving. -Slicing from Formal Sematics: Chisel -- EasyInterface: A toolkit for rapid development of GUIs for research prototype tools -- Software Product Lines -- Family-Based Model Checking with mCRL2 -- Variability-specific Abstraction Refinement for Family-based Model Checking -- A Unified and Formal Programming Model for Deltas and Traits. |
| Record Nr. | UNISA-996466188203316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2017 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Fundamental Approaches to Software Engineering : 20th International Conference, FASE 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings / / edited by Marieke Huisman, Julia Rubin
| Fundamental Approaches to Software Engineering : 20th International Conference, FASE 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings / / edited by Marieke Huisman, Julia Rubin |
| Edizione | [1st ed. 2017.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2017 |
| Descrizione fisica | 1 online resource (XIII, 444 p. 130 illus.) |
| Disciplina | 005.1 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Software engineering
Compilers (Computer programs) Computer science Machine theory Software Engineering Compilers and Interpreters Computer Science Logic and Foundations of Programming Formal Languages and Automata Theory |
| ISBN | 3-662-54494-6 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Learning and Inference -- Should We Learn Probabilistic Models for Model Checking? A New Approach and an Empirical Study -- Bordeaux: a tool for thinking outside the box -- Test Selection -- Bucketing Failing Tests via Symbolic Analysis -- Selective Bisection Debugging. - On the Effectiveness of Bug Predictors with Procedural Systems: a Quantitative Study -- Program and System Analysis -- Inference and Evolution of TypeScript Declaration Files -- Explicit Connection Actions in Multiparty Session Types -- Change and Delay Contracts for Hybrid System Component Verification. - Precise Version Control of Trees with Line-based Version Control Systems -- Graph Modelling and Transformation -- StaticGen: Static Generation of UML Sequence Diagrams -- Inter-Model Consistency Checking using Triple Graph Grammars and Linear Optimization Techniques -- GTS Families for the Flexible Composition of Graph Transformation Systems -- Symbolic Model Generation for Graph Properties. - Model Transformations -- Traceability Mappings as a Fundamental Instrument in Model Transformations -- Reusing Model Transformations through Typing Requirement Models -- Change-preserving model repair. -A deductive approach for fault localization in ATL model transformations. -Configuration and Synthesis -- OpenSAW: Open Security Analysis Workbench -- Visual Configuration of Mobile Privacy Policies -- Automated Workarounds from Java Program Specifications based on SAT Solving. -Slicing from Formal Sematics: Chisel -- EasyInterface: A toolkit for rapid development of GUIs for research prototype tools -- Software Product Lines -- Family-Based Model Checking with mCRL2 -- Variability-specific Abstraction Refinement for Family-based Model Checking -- A Unified and Formal Programming Model for Deltas and Traits. |
| Record Nr. | UNINA-9910483259203321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2017 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Integrated Formal Methods [[electronic resource] ] : 12th International Conference, IFM 2016, Reykjavik, Iceland, June 1-5, 2016, Proceedings / / edited by Erika Ábrahám, Marieke Huisman
| Integrated Formal Methods [[electronic resource] ] : 12th International Conference, IFM 2016, Reykjavik, Iceland, June 1-5, 2016, Proceedings / / edited by Erika Ábrahám, Marieke Huisman |
| Edizione | [1st ed. 2016.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2016 |
| Descrizione fisica | 1 online resource (XIV, 538 p. 145 illus.) |
| Disciplina | 004.0151 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Software engineering
Computer logic Programming languages (Electronic computers) Mathematical logic Software Engineering Logics and Meanings of Programs Programming Languages, Compilers, Interpreters Mathematical Logic and Formal Languages |
| ISBN | 3-319-33693-2 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Contributions -- Can Formal Methods Improve the Efficiency of Code Reviews.-Symbolic Computation and Automated Reasoning for Program Analysis -- Program verification -- On Type Checking Delta-Oriented Product Lines -- Verifying a priority scheduler for an SCJ runtime environment -- Why Just Boogie? Translating Between Intermediate Verification Languages -- Probabilistic systems -- Statistical Approximation of Optimal Schedulers for Probabilistic Timed Automata -- Probabilistic Formal Analysis of App Usage to Inform Redesign -- Extension of PRISM by Synthesis of Optimal Timeouts in Fixed-Delay CTMC -- Concurrency -- Monitoring Multi-threaded Component-Based Systems -- A Generalised Theory of Interface Automata, Component Compatibility and Error -- On Implementing a Monitor-Oriented Programming Framework for Actor Systems -- Towards a Thread-Local Proof Technique for Starvation Freedom -- Reasoning about Inheritance and Unrestricted Reuse in Object-Oriented Concurrent Systems -- A Formal Model of the Safety-Critical Java Level 2 Paradigm -- Safety and liveness -- Deciding Monadic Second Order Logic over omega-words by Specialized Finite Automata -- Property Preservation for Extension Patterns of State Transition Diagrams -- Symbolic Reachability Analysis of B through ProB and LTSmin -- Model learning -- Enhancing Automata Learning by Log-Based Metrics -- Refactoring of Legacy Software using Model Learning and Equivalence Checking: an Industrial Experience Report -- On Robust Malware Classifiers by Verifying Unwanted Behaviours -- SAT and SMT solving -- Efficient Deadlock-Freedom Checking using Local Analysis and SAT Solving -- SMT Solvers for Validation of B and Event-B models -- Avoiding Medication Conflicts for Patients with Multimorbidities -- Testing -- Temporal Random Testing for Spark Streaming -- Combining Static Analysis and Testing for Deadlock Detection -- Fuzzing JavaScript Engine APIs -- Theorem proving and constraint satisfaction -- A Component-based Approach to Hybrid Systems Safety Verification -- Verifying Pointer Programs using Separation Logic and Invariant Based Programming in Isabelle -- A Constraint Satisfaction Method for Configuring Non-Local Service Interfaces -- Case studies -- Rule-based Consistency Checking of Railway Infrastructure Designs -- Formal Verification of Safety PLC Based Control Software -- Enabling Static Driver Verifier using Microsoft Azure. |
| Record Nr. | UNISA-996465780903316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2016 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Integrated Formal Methods : 12th International Conference, IFM 2016, Reykjavik, Iceland, June 1-5, 2016, Proceedings / / edited by Erika Ábrahám, Marieke Huisman
| Integrated Formal Methods : 12th International Conference, IFM 2016, Reykjavik, Iceland, June 1-5, 2016, Proceedings / / edited by Erika Ábrahám, Marieke Huisman |
| Edizione | [1st ed. 2016.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2016 |
| Descrizione fisica | 1 online resource (XIV, 538 p. 145 illus.) |
| Disciplina | 004.0151 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Software engineering
Computer science Compilers (Computer programs) Machine theory Software Engineering Computer Science Logic and Foundations of Programming Compilers and Interpreters Formal Languages and Automata Theory |
| ISBN | 3-319-33693-2 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Contributions -- Can Formal Methods Improve the Efficiency of Code Reviews.-Symbolic Computation and Automated Reasoning for Program Analysis -- Program verification -- On Type Checking Delta-Oriented Product Lines -- Verifying a priority scheduler for an SCJ runtime environment -- Why Just Boogie? Translating Between Intermediate Verification Languages -- Probabilistic systems -- Statistical Approximation of Optimal Schedulers for Probabilistic Timed Automata -- Probabilistic Formal Analysis of App Usage to Inform Redesign -- Extension of PRISM by Synthesis of Optimal Timeouts in Fixed-Delay CTMC -- Concurrency -- Monitoring Multi-threaded Component-Based Systems -- A Generalised Theory of Interface Automata, Component Compatibility and Error -- On Implementing a Monitor-Oriented Programming Framework for Actor Systems -- Towards a Thread-Local Proof Technique for Starvation Freedom -- Reasoning about Inheritance and Unrestricted Reuse in Object-Oriented Concurrent Systems -- A Formal Model of the Safety-Critical Java Level 2 Paradigm -- Safety and liveness -- Deciding Monadic Second Order Logic over omega-words by Specialized Finite Automata -- Property Preservation for Extension Patterns of State Transition Diagrams -- Symbolic Reachability Analysis of B through ProB and LTSmin -- Model learning -- Enhancing Automata Learning by Log-Based Metrics -- Refactoring of Legacy Software using Model Learning and Equivalence Checking: an Industrial Experience Report -- On Robust Malware Classifiers by Verifying Unwanted Behaviours -- SAT and SMT solving -- Efficient Deadlock-Freedom Checking using Local Analysis and SAT Solving -- SMT Solvers for Validation of B and Event-B models -- Avoiding Medication Conflicts for Patients with Multimorbidities -- Testing -- Temporal Random Testing for Spark Streaming -- Combining Static Analysis and Testing for Deadlock Detection -- Fuzzing JavaScript Engine APIs -- Theorem proving and constraint satisfaction -- A Component-based Approach to Hybrid Systems Safety Verification -- Verifying Pointer Programs using Separation Logic and Invariant Based Programming in Isabelle -- A Constraint Satisfaction Method for Configuring Non-Local Service Interfaces -- Case studies -- Rule-based Consistency Checking of Railway Infrastructure Designs -- Formal Verification of Safety PLC Based Control Software -- Enabling Static Driver Verifier using Microsoft Azure. |
| Record Nr. | UNINA-9910484921703321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2016 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
