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.
Abstract State Machines, Alloy, B, TLA, VDM, and Z [[electronic resource] ] : 6th International Conference, ABZ 2018, Southampton, UK, June 5–8, 2018, Proceedings / / edited by Michael Butler, Alexander Raschke, Thai Son Hoang, Klaus Reichl
| Abstract State Machines, Alloy, B, TLA, VDM, and Z [[electronic resource] ] : 6th International Conference, ABZ 2018, Southampton, UK, June 5–8, 2018, Proceedings / / edited by Michael Butler, Alexander Raschke, Thai Son Hoang, Klaus Reichl |
| Edizione | [1st ed. 2018.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018 |
| Descrizione fisica | 1 online resource (XIV, 432 p. 83 illus.) |
| Disciplina | 006.31 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Machine theory
Algorithms Computer science Compilers (Computer programs) Artificial intelligence Formal Languages and Automata Theory Computer Science Logic and Foundations of Programming Compilers and Interpreters Artificial Intelligence |
| ISBN | 3-319-91271-2 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- Translation and Transformation -- Analysis and Tests -- Reals and Hybrid Systems -- Refinement -- Hybrid ERTMS Case Study -- Short Papers. |
| Record Nr. | UNISA-996465825303316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Abstract State Machines, Alloy, B, TLA, VDM, and Z [[electronic resource] ] : 6th International Conference, ABZ 2018, Southampton, UK, June 5–8, 2018, Proceedings / / edited by Michael Butler, Alexander Raschke, Thai Son Hoang, Klaus Reichl
| Abstract State Machines, Alloy, B, TLA, VDM, and Z [[electronic resource] ] : 6th International Conference, ABZ 2018, Southampton, UK, June 5–8, 2018, Proceedings / / edited by Michael Butler, Alexander Raschke, Thai Son Hoang, Klaus Reichl |
| Edizione | [1st ed. 2018.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018 |
| Descrizione fisica | 1 online resource (XIV, 432 p. 83 illus.) |
| Disciplina | 006.31 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Machine theory
Algorithms Computer science Compilers (Computer programs) Artificial intelligence Formal Languages and Automata Theory Computer Science Logic and Foundations of Programming Compilers and Interpreters Artificial Intelligence |
| ISBN | 3-319-91271-2 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- Translation and Transformation -- Analysis and Tests -- Reals and Hybrid Systems -- Refinement -- Hybrid ERTMS Case Study -- Short Papers. |
| Record Nr. | UNINA-9910349429803321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Abstract State Machines, Alloy, B, TLA, VDM, and Z [[electronic resource] ] : 5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings / / edited by Michael Butler, Klaus-Dieter Schewe, Atif Mashkoor, Miklos Biro
| Abstract State Machines, Alloy, B, TLA, VDM, and Z [[electronic resource] ] : 5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings / / edited by Michael Butler, Klaus-Dieter Schewe, Atif Mashkoor, Miklos Biro |
| Edizione | [1st ed. 2016.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2016 |
| Descrizione fisica | 1 online resource (XXI, 426 p. 143 illus.) |
| Disciplina | 004 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Machine theory
Computer science Software engineering Compilers (Computer programs) Formal Languages and Automata Theory Computer Science Logic and Foundations of Programming Theory of Computation Software Engineering Compilers and Interpreters |
| ISBN | 3-319-33600-2 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Modeling Distributed Algorithms by Abstract State Machines Compared to Petri Nets -- A Universal Control Construct for Abstract State Machines -- Encoding TLA+ into Many-Sorted First-Order Logic -- Proving Determinacy of PharOS in TLA+ -- A Rigorous Correctness Proof for Pastry -- Enabling Analysis for B and Event-B -- A Compact Encoding of Sequential ASMs in Event-B -- Proof Assisted Symbolic Model Checking for B and Event-B -- On Component-based Reuse for Event-B -- Using B and ProB for Data Validation Projects -- Generating Event-B Specifications from Algorithm Descriptions -- Formal Proofs of Termination Detection for Local Computations by Refinement-Based Compositions -- How to Select the Suitable Formal Method for an Industrial Application: A Survey -- Unified Syntax for Abstract State Machines -- A Relational Encoding for a Clash-Free Subset of ASMs -- Towards an ASM Thesis for Reflective Sequential Algorithms -- A Model-based Transformation Approach to Reuse and Retarget CASM Specifications -- Modeling a Discrete Wet-Dry Algorithm for Hurricane Storm Surge in Alloy -- `The Tinker' for Rodin -- A Graphical Tool for Event Refinement Structures in Event-B -- Rodin Platform Why3 plug-in -- Semi-Automated Design Space Exploration for Formal Modelling -- Handling Continuous Functions in Hybrid Systems Reconfigurations: A Formal Event-B Development -- UC-B: Use Case Modelling with Event-B -- Interactive Model Repair by Synthesis -- SysML2B: Automatic Tool for B Project Graphical Architecture Design using SysML -- Mechanized Refinement of Communication Models with TLA+ -- A Super Industrial Application of PSGraph -- The Hemodialysis Machine Case Study -- How to Assure Correctness and Safety of Medical Software: The Hemodialysis Machine Case Study -- Validating the Requirements and Design of a Hemodialysis Machine Using iUML-B, BMotionStudio, and Co-simulation -- Hemodialysis Machine in Hybrid Event-B -- Modeling a Hemodialysis Machine using Algebraic State-Transition Diagrams and B-like Methods -- Modelling the Haemodialysis Machine with Circus. |
| Record Nr. | UNISA-996465777503316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2016 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Abstract State Machines, Alloy, B, TLA, VDM, and Z [[electronic resource] ] : 5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings / / edited by Michael Butler, Klaus-Dieter Schewe, Atif Mashkoor, Miklos Biro
| Abstract State Machines, Alloy, B, TLA, VDM, and Z [[electronic resource] ] : 5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings / / edited by Michael Butler, Klaus-Dieter Schewe, Atif Mashkoor, Miklos Biro |
| Edizione | [1st ed. 2016.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2016 |
| Descrizione fisica | 1 online resource (XXI, 426 p. 143 illus.) |
| Disciplina | 004 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Machine theory
Computer science Software engineering Compilers (Computer programs) Formal Languages and Automata Theory Computer Science Logic and Foundations of Programming Theory of Computation Software Engineering Compilers and Interpreters |
| ISBN | 3-319-33600-2 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Modeling Distributed Algorithms by Abstract State Machines Compared to Petri Nets -- A Universal Control Construct for Abstract State Machines -- Encoding TLA+ into Many-Sorted First-Order Logic -- Proving Determinacy of PharOS in TLA+ -- A Rigorous Correctness Proof for Pastry -- Enabling Analysis for B and Event-B -- A Compact Encoding of Sequential ASMs in Event-B -- Proof Assisted Symbolic Model Checking for B and Event-B -- On Component-based Reuse for Event-B -- Using B and ProB for Data Validation Projects -- Generating Event-B Specifications from Algorithm Descriptions -- Formal Proofs of Termination Detection for Local Computations by Refinement-Based Compositions -- How to Select the Suitable Formal Method for an Industrial Application: A Survey -- Unified Syntax for Abstract State Machines -- A Relational Encoding for a Clash-Free Subset of ASMs -- Towards an ASM Thesis for Reflective Sequential Algorithms -- A Model-based Transformation Approach to Reuse and Retarget CASM Specifications -- Modeling a Discrete Wet-Dry Algorithm for Hurricane Storm Surge in Alloy -- `The Tinker' for Rodin -- A Graphical Tool for Event Refinement Structures in Event-B -- Rodin Platform Why3 plug-in -- Semi-Automated Design Space Exploration for Formal Modelling -- Handling Continuous Functions in Hybrid Systems Reconfigurations: A Formal Event-B Development -- UC-B: Use Case Modelling with Event-B -- Interactive Model Repair by Synthesis -- SysML2B: Automatic Tool for B Project Graphical Architecture Design using SysML -- Mechanized Refinement of Communication Models with TLA+ -- A Super Industrial Application of PSGraph -- The Hemodialysis Machine Case Study -- How to Assure Correctness and Safety of Medical Software: The Hemodialysis Machine Case Study -- Validating the Requirements and Design of a Hemodialysis Machine Using iUML-B, BMotionStudio, and Co-simulation -- Hemodialysis Machine in Hybrid Event-B -- Modeling a Hemodialysis Machine using Algebraic State-Transition Diagrams and B-like Methods -- Modelling the Haemodialysis Machine with Circus. |
| Record Nr. | UNINA-9910483395003321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2016 | ||
| 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] ] : 17th International Conference on Formal Engineering Methods, ICFEM 2015, Paris, France, November 3-5, 2015, Proceedings / / edited by Michael Butler, Sylvain Conchon, Fatiha Zaïdi
| Formal Methods and Software Engineering [[electronic resource] ] : 17th International Conference on Formal Engineering Methods, ICFEM 2015, Paris, France, November 3-5, 2015, Proceedings / / edited by Michael Butler, Sylvain Conchon, Fatiha Zaïdi |
| Edizione | [1st ed. 2015.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 |
| Descrizione fisica | 1 online resource (XXV, 436 p. 150 illus. in color.) |
| Disciplina | 004 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Software engineering
Computer programming Programming languages (Electronic computers) Algorithms Mathematical logic Computer communication systems Software Engineering Programming Techniques Programming Languages, Compilers, Interpreters Algorithm Analysis and Problem Complexity Mathematical Logic and Formal Languages Computer Communication Networks |
| ISBN | 3-319-25423-5 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNINA-9910483127203321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Formal Methods and Software Engineering [[electronic resource] ] : 17th International Conference on Formal Engineering Methods, ICFEM 2015, Paris, France, November 3-5, 2015, Proceedings / / edited by Michael Butler, Sylvain Conchon, Fatiha Zaïdi
| Formal Methods and Software Engineering [[electronic resource] ] : 17th International Conference on Formal Engineering Methods, ICFEM 2015, Paris, France, November 3-5, 2015, Proceedings / / edited by Michael Butler, Sylvain Conchon, Fatiha Zaïdi |
| Edizione | [1st ed. 2015.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 |
| Descrizione fisica | 1 online resource (XXV, 436 p. 150 illus. in color.) |
| Disciplina | 004 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Software engineering
Computer programming Programming languages (Electronic computers) Algorithms Mathematical logic Computer communication systems Software Engineering Programming Techniques Programming Languages, Compilers, Interpreters Algorithm Analysis and Problem Complexity Mathematical Logic and Formal Languages Computer Communication Networks |
| ISBN | 3-319-25423-5 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNISA-996466223303316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Formal methods and software engineering : 9th International Conference on Formal Engineering Methods, ICFEM 2007, Boca Raton, FL, USA, November 14-15, 2007 : proceedings / / Michael Butler, Michael G. Hinchey, Maria M. Larrondo-Petrie (editors)
| Formal methods and software engineering : 9th International Conference on Formal Engineering Methods, ICFEM 2007, Boca Raton, FL, USA, November 14-15, 2007 : proceedings / / Michael Butler, Michael G. Hinchey, Maria M. Larrondo-Petrie (editors) |
| Edizione | [1st ed. 2007.] |
| Pubbl/distr/stampa | Berlin : , : Springer, , [2007] |
| Descrizione fisica | 1 online resource (VIII, 387 p.) |
| Disciplina | 004.0151 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Formal methods (Computer science)
Software engineering |
| ISBN | 3-540-76650-2 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- A System Development Process with Event-B and the Rodin Platform -- Challenges in Software Certification -- Security and Knowledge -- Integrating Formal Methods with System Management -- Formal Engineering of XACML Access Control Policies in VDM++ -- A Verification Framework for Agent Knowledge -- Embedded Systems -- From Model-Based Design to Formal Verification of Adaptive Embedded Systems -- Machine-Assisted Proof Support for Validation Beyond Simulink -- VeSTA: A Tool to Verify the Correct Integration of a Component in a Composite Timed System -- Testing -- Integrating Specification-Based Review and Testing for Detecting Errors in Programs -- Testing for Refinement in CSP -- Reducing Test Sequence Length Using Invertible Sequences -- Automated Analysis -- Model Checking with SAT-Based Characterization of ACTL Formulas -- Automating Refinement Checking in Probabilistic System Design -- Model Checking in Practice: Analysis of Generic Bootloader Using SPIN -- Model Checking Propositional Projection Temporal Logic Based on SPIN -- Hardware -- A Denotational Semantics for Handel-C Hardware Compilation -- Automatic Generation of Verified Concurrent Hardware -- Modeling and Verification of Master/Slave Clock Synchronization Using Hybrid Automata and Model-Checking -- Concurrency -- Efficient Symbolic Execution of Large Quantifications in a Process Algebra -- Formalizing SANE Virtual Processor in Thread Algebra -- Calculating and Composing Progress Properties in Terms of the Leads-to Relation -- Erratum -- Erratum to: Challenges in Software Certification. |
| Record Nr. | UNISA-996465956103316 |
| Berlin : , : Springer, , [2007] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Formal methods and software engineering : 9th International Conference on Formal Engineering Methods, ICFEM 2007, Boca Raton, FL, USA, November 14-15, 2007 : proceedings / / Michael Butler, Michael G. Hinchey, Maria M. Larrondo-Petrie (editors)
| Formal methods and software engineering : 9th International Conference on Formal Engineering Methods, ICFEM 2007, Boca Raton, FL, USA, November 14-15, 2007 : proceedings / / Michael Butler, Michael G. Hinchey, Maria M. Larrondo-Petrie (editors) |
| Edizione | [1st ed. 2007.] |
| Pubbl/distr/stampa | Berlin : , : Springer, , [2007] |
| Descrizione fisica | 1 online resource (VIII, 387 p.) |
| Disciplina | 004.0151 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Formal methods (Computer science)
Software engineering |
| ISBN | 3-540-76650-2 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- A System Development Process with Event-B and the Rodin Platform -- Challenges in Software Certification -- Security and Knowledge -- Integrating Formal Methods with System Management -- Formal Engineering of XACML Access Control Policies in VDM++ -- A Verification Framework for Agent Knowledge -- Embedded Systems -- From Model-Based Design to Formal Verification of Adaptive Embedded Systems -- Machine-Assisted Proof Support for Validation Beyond Simulink -- VeSTA: A Tool to Verify the Correct Integration of a Component in a Composite Timed System -- Testing -- Integrating Specification-Based Review and Testing for Detecting Errors in Programs -- Testing for Refinement in CSP -- Reducing Test Sequence Length Using Invertible Sequences -- Automated Analysis -- Model Checking with SAT-Based Characterization of ACTL Formulas -- Automating Refinement Checking in Probabilistic System Design -- Model Checking in Practice: Analysis of Generic Bootloader Using SPIN -- Model Checking Propositional Projection Temporal Logic Based on SPIN -- Hardware -- A Denotational Semantics for Handel-C Hardware Compilation -- Automatic Generation of Verified Concurrent Hardware -- Modeling and Verification of Master/Slave Clock Synchronization Using Hybrid Automata and Model-Checking -- Concurrency -- Efficient Symbolic Execution of Large Quantifications in a Process Algebra -- Formalizing SANE Virtual Processor in Thread Algebra -- Calculating and Composing Progress Properties in Terms of the Leads-to Relation -- Erratum -- Erratum to: Challenges in Software Certification. |
| Record Nr. | UNINA-9910484765603321 |
| Berlin : , : Springer, , [2007] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Integrated formal methods : Third International Conference, IFM 2002, Turku, Finland, May 15-18, 2002 : proceedings / / Michael Butler, Luigia Petre, Kaisa Sere, eds
| Integrated formal methods : Third International Conference, IFM 2002, Turku, Finland, May 15-18, 2002 : proceedings / / Michael Butler, Luigia Petre, Kaisa Sere, eds |
| Edizione | [1st ed. 2002.] |
| Pubbl/distr/stampa | Berlin, Germany ; ; New York, New York : , : Springer, , [2002] |
| Descrizione fisica | 1 online resource (X, 401 p.) |
| Disciplina | 004/.01/51 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico | Formal methods (Computer science) |
| ISBN | 3-540-47884-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talk: Eran Gery -- Rhapsody: A Complete Life-Cycle Model-Based Development System -- Integration, Simulation, Animation -- An Integrated Semantics for UML Class, Object and State Diagrams Based on Graph Transformation -- Stochastic Process Algebras Meet Eden -- From Specifcation to Verifcation -- From Implicit Specifications to Explicit Designs in Reactive System Development -- Basic-REAL: Integrated Approach for Design, Specification and Verification of Distributed Systems -- Assume-Guarantee Algorithms for Automatic Detection of Software Failures -- Statecharts and B: Integration and Translation -- Contributions for Modelling UML State-Charts in B -- Translating Statecharts to B -- Invited Talk: Shmuel Katz -- A Framework for Translating Models and Specifications -- Model Checkers and Theorem Provers -- Model Checking Object-Z Using ASM -- Formalization of Cadence SPW Fixed-Point Arithmetic in HOL -- Formally Linking MDG and HOL Based on a Verified MDG System -- Links between Object-Z and CSP -- Refinement in Object-Z and CSP -- Combining Specification Techniques for Processes, Data and Time -- An Integration of Real-Time Object-Z and CSP for Specifying Concurrent Real-Time Systems -- Invited Talk: Stuart Kent -- Model Driven Engineering -- Combining Graphical and Formal Approaches -- The Design of a Tool-Supported Graphical Notation for Timed CSP -- Combining Graphical and Formal Development of Open Distributed Systems -- Translations between Textual Transition Systems and Petri Nets -- Refinement and Proof -- Specification and Proof of Liveness Properties under Fairness Assumptions in B Event Systems -- Minimally and Maximally Abstract Retrenchments. |
| Record Nr. | UNINA-9910143906703321 |
| Berlin, Germany ; ; New York, New York : , : Springer, , [2002] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
