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.
Formal method : industrial use from model to the code / / editor, Jean-Louis Boulanger
| Formal method : industrial use from model to the code / / editor, Jean-Louis Boulanger |
| Edizione | [1st ed.] |
| Pubbl/distr/stampa | London : , : ISTE |
| Descrizione fisica | 1 online resource (376 pages) |
| Disciplina | 385.0285/53 |
| Altri autori (Persone) | BoulangerJean-Louis |
| Collana | Industrial implementation of formal methods series |
| Soggetto topico |
Railroads - Management - Data processing
Formal methods (Computer science) Application software - Development |
| ISBN |
1-118-61437-2
1-118-56189-9 1-299-31507-0 1-118-61438-0 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | From classic languages to formal methods -- Formal method in railway, the first complex application : SAET-METEOR -- B method and B tools -- Model-based design using Simulink : modeling, code generation, verification, and validation -- Proof of global properties with the aid of the Simulink Design verifier proof tool -- SCADE : implementation and applications -- GATel : a V & V platform for scade models -- Control build. |
| Record Nr. | UNINA-9910820783003321 |
| London : , : ISTE | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Formal methods : 25th international symposium, FM 2023, Lübeck, Germany, March 6-10, 2023, proceedings / / edited by Marsha Chechik, Joost-Pieter Katoen, and Martin Leucker
| Formal methods : 25th international symposium, FM 2023, Lübeck, Germany, March 6-10, 2023, proceedings / / edited by Marsha Chechik, Joost-Pieter Katoen, and Martin Leucker |
| Edizione | [1st ed. 2023.] |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2023] |
| Descrizione fisica | 1 online resource (661 pages) |
| Disciplina | 004.0151 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico | Formal methods (Computer science) |
| ISBN | 3-031-27481-4 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Keynotes -- Symbolic Computation in Automated Program Reasoning -- The next big thing: from embedded systems to embodied actors -- Intelligent and Dependable Decision-Making Under Uncertainty -- A Coq formalization of Lebesgue Induction Principle and Tonelli’s Theorem -- SAT/SMT -- Railway Scheduling Using Boolean Satisfiability Modulo Simulations -- SMT Sampling via Model-Guided Approximation -- Efficient SMT-based Network Fault Tolerance Verification -- Verification I -- Formalising the Prevention of Microarchitectural Timing Channels by Operating Systems -- Can we Communicate? Using Dynamic Logic to Verify Team Automata -- The ScalaFix equation solver -- HHLPy: Practical Verification of Hybrid Systems using Hoare Logic -- Quantitative Verification -- symQV: Automated Symbolic Verification of Quantum Programs -- PFL: a Probabilistic Logic for Fault Trees -- Energy Buechi Problems -- QMaude: quantitative specification and verification in rewriting logic -- Concurrency and Memory Models -- Minimisation of Spatial Models using Branching Bisimilarity -- Reasoning about Promises in Weak Memory Models with Event Structures -- A fine-grained semantics for arrays and pointers under weak memory models -- VeyMont: Parallelising Verified Programs instead of Verifying Parallel Programs -- Verification 2 -- Verifying At the Level of Java Bytecode -- Abstract Alloy Instances -- Monitoring the Internet Computer -- Word Equations in Synergy with Regular Constraints -- Formal Methods in AI -- Verifying Feedforward Neural Networks for Classification in Isabelle/HOL -- SMPT: A Testbed for Reachabilty Methods in Generalized Petri Nets -- The Octatope Abstract Domain for Verification of Neural Networks -- Program Semantics and Verification Technique for AI-centred Programs -- Safety and Reliability -- Tableaux for Realizability of Safety Specifications -- A Decision Diagram Operation for Reachability -- Formal Modelling of Safety Architecture for Responsibility-Aware Autonomous Vehicle via Event-B Refinement -- A Runtime Environment for Contract Automata -- Industry Day -- Formal and Executable Semantics of the Ethereum Virtual Machine in Dafny -- Shifting Left for Early Detection of Machine-Learning Bugs -- A Systematic Approach to Automotive Security -- Specification-Guided Critical Scenario Identification for Automated Driving -- Runtime Monitoring for Out-of-Distribution Detection in Object Detection Neural Networks -- Backdoor Mitigation in Deep Neural Networks via Strategic Retraining -- veriFIRE: Verifying an Industrial, Learning-Based Wildfire Detection System. |
| Record Nr. | UNINA-9910678257703321 |
| Cham, Switzerland : , : Springer, , [2023] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Formal methods : 25th international symposium, FM 2023, Lübeck, Germany, March 6-10, 2023, proceedings / / edited by Marsha Chechik, Joost-Pieter Katoen, and Martin Leucker
| Formal methods : 25th international symposium, FM 2023, Lübeck, Germany, March 6-10, 2023, proceedings / / edited by Marsha Chechik, Joost-Pieter Katoen, and Martin Leucker |
| Edizione | [1st ed. 2023.] |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2023] |
| Descrizione fisica | 1 online resource (661 pages) |
| Disciplina | 004.0151 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico | Formal methods (Computer science) |
| ISBN | 3-031-27481-4 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Keynotes -- Symbolic Computation in Automated Program Reasoning -- The next big thing: from embedded systems to embodied actors -- Intelligent and Dependable Decision-Making Under Uncertainty -- A Coq formalization of Lebesgue Induction Principle and Tonelli’s Theorem -- SAT/SMT -- Railway Scheduling Using Boolean Satisfiability Modulo Simulations -- SMT Sampling via Model-Guided Approximation -- Efficient SMT-based Network Fault Tolerance Verification -- Verification I -- Formalising the Prevention of Microarchitectural Timing Channels by Operating Systems -- Can we Communicate? Using Dynamic Logic to Verify Team Automata -- The ScalaFix equation solver -- HHLPy: Practical Verification of Hybrid Systems using Hoare Logic -- Quantitative Verification -- symQV: Automated Symbolic Verification of Quantum Programs -- PFL: a Probabilistic Logic for Fault Trees -- Energy Buechi Problems -- QMaude: quantitative specification and verification in rewriting logic -- Concurrency and Memory Models -- Minimisation of Spatial Models using Branching Bisimilarity -- Reasoning about Promises in Weak Memory Models with Event Structures -- A fine-grained semantics for arrays and pointers under weak memory models -- VeyMont: Parallelising Verified Programs instead of Verifying Parallel Programs -- Verification 2 -- Verifying At the Level of Java Bytecode -- Abstract Alloy Instances -- Monitoring the Internet Computer -- Word Equations in Synergy with Regular Constraints -- Formal Methods in AI -- Verifying Feedforward Neural Networks for Classification in Isabelle/HOL -- SMPT: A Testbed for Reachabilty Methods in Generalized Petri Nets -- The Octatope Abstract Domain for Verification of Neural Networks -- Program Semantics and Verification Technique for AI-centred Programs -- Safety and Reliability -- Tableaux for Realizability of Safety Specifications -- A Decision Diagram Operation for Reachability -- Formal Modelling of Safety Architecture for Responsibility-Aware Autonomous Vehicle via Event-B Refinement -- A Runtime Environment for Contract Automata -- Industry Day -- Formal and Executable Semantics of the Ethereum Virtual Machine in Dafny -- Shifting Left for Early Detection of Machine-Learning Bugs -- A Systematic Approach to Automotive Security -- Specification-Guided Critical Scenario Identification for Automated Driving -- Runtime Monitoring for Out-of-Distribution Detection in Object Detection Neural Networks -- Backdoor Mitigation in Deep Neural Networks via Strategic Retraining -- veriFIRE: Verifying an Industrial, Learning-Based Wildfire Detection System. |
| Record Nr. | UNISA-996517755403316 |
| Cham, Switzerland : , : Springer, , [2023] | ||
| 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 : foundations and applications : 24th Brazilian Symposium, SBMF 2021, virtual event, December 6-10, 2021 : proceedings / / Sérgio Campos, Marius Minea (editors)
| Formal methods : foundations and applications : 24th Brazilian Symposium, SBMF 2021, virtual event, December 6-10, 2021 : proceedings / / Sérgio Campos, Marius Minea (editors) |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2021] |
| Descrizione fisica | 1 online resource (149 pages) |
| Disciplina | 004.0151 |
| Collana | Lecture notes in computer science |
| Soggetto topico | Formal methods (Computer science) |
| ISBN | 3-030-92137-9 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Preface -- Organization -- Contents -- A Two-Level Approach Based on Model Checking to Support Architecture Conformance Checking -- 1 Introduction -- 2 Theoretical Background -- 2.1 Model Checking -- 2.2 Temporal Logic and Hybrid Logic -- 2.3 Software Versioning -- 3 The Proposed Method -- 3.1 Call Graphs as Kripke Structures -- 3.2 Version Graphs as Kripke Structures -- 3.3 The Proposed Logic: A Two-Level Temporal Logic for Specifications Checking -- 3.4 Examples -- 4 Conclusion and Future Works -- References -- Statistical Model Checking for Traffic Models -- 1 Introduction -- 2 Background -- 2.1 SMC and MultiVeStA -- 2.2 SUMO - Simulation of Urban MObility -- 2.3 Car-Following and Lane Changing Models -- 3 Integration of MultiVeStA and SUMO Simulator -- 3.1 Initial Step -- 3.2 Integration -- 4 Simulation Experiments and Results -- 4.1 Simple Queries -- 4.2 Query 1: Behaviour on Emergency Vehicles -- 4.3 Query 2: Traffic Load Comparison -- 4.4 Query 3: Load Conditions for Traffic Jams -- 4.5 Query 4: Impending Drop in Traffic -- 4.6 Running Times -- 5 Conclusion and Future Work -- References -- Visual Specification of Properties for Robotic Designs -- 1 Introduction -- 2 Background -- 2.1 RoboChart -- 2.2 UML Activity Diagram -- 2.3 CSP Notation, Templates and Tools Used in the Work -- 3 Diagrammatic Language for Properties -- 3.1 Language Syntax -- 3.2 Language Semantics -- 4 Tool Support -- 5 Related Work -- 6 Conclusion -- References -- Model Checking and Strategy Synthesis for Multi-agent Systems for Resource Allocation -- 1 Introduction -- 2 Multi-agent Systems for Resource Allocation -- 3 Propositional Logic Encoding -- 3.1 Overall Encoding -- 3.2 Basic Encodings -- 3.3 Properties of the Encoding -- 4 Algorithm -- 5 Implementation and Experiments -- 6 Related Work -- 7 Conclusion and Outlook -- References.
Temporal Reasoning Through Automatic Translation of tock-CSP into Timed Automata -- 1 Introduction -- 2 Background -- 3 An Overview of the Translation Technique -- 4 Evaluation -- 4.1 Experimental Evaluation -- 4.2 Mathematical Proof -- 5 Related Work and Conclusions -- References -- Module Integration Using Graph Grammars (MIGRATE) -- 1 Introduction -- 2 Graph Grammars -- 3 Illustration of the Proposed Approach -- 4 Module Nets -- 5 MIGRATE Approach -- 5.1 Translation -- 5.2 Verification -- 6 Related Work -- 7 Conclusion -- References -- Cost Analysis for an Actor-Based Workflow Modelling Language -- 1 Introduction -- 2 Formal Workflow Modelling Language Rpl -- 2.1 The Syntax of Rpl -- 2.2 The Semantics of Rpl -- 3 Analysis of Rpl Program -- 3.1 Synchronisation Schema -- 3.2 Accumulated Costs -- 3.3 Translation Function -- 4 Properties -- 5 Related Work -- 6 Conclusion -- References -- Minimization of the Number of Clocks for Timed Scenarios -- 1 Introduction -- 2 Preliminaries -- 2.1 Timed Automata -- 2.2 Timed Scenarios -- 3 A New Optimization Algorithm -- 3.1 Cyclic Dependencies -- 3.2 Cyclic Dependencies and Equality Constraints -- 3.3 C(Ds) with Cyclic Dependencies -- 3.4 Resolving Cyclic Dependencies -- 3.5 The Optimization Algorithm -- 4 Conclusions -- References -- Author Index. |
| Record Nr. | UNISA-996464506203316 |
| Cham, Switzerland : , : Springer, , [2021] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Formal methods : foundations and applications : 24th Brazilian Symposium, SBMF 2021, virtual event, December 6-10, 2021 : proceedings / / Sérgio Campos, Marius Minea (editors)
| Formal methods : foundations and applications : 24th Brazilian Symposium, SBMF 2021, virtual event, December 6-10, 2021 : proceedings / / Sérgio Campos, Marius Minea (editors) |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2021] |
| Descrizione fisica | 1 online resource (149 pages) |
| Disciplina | 004.0151 |
| Collana | Lecture notes in computer science |
| Soggetto topico | Formal methods (Computer science) |
| ISBN | 3-030-92137-9 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Preface -- Organization -- Contents -- A Two-Level Approach Based on Model Checking to Support Architecture Conformance Checking -- 1 Introduction -- 2 Theoretical Background -- 2.1 Model Checking -- 2.2 Temporal Logic and Hybrid Logic -- 2.3 Software Versioning -- 3 The Proposed Method -- 3.1 Call Graphs as Kripke Structures -- 3.2 Version Graphs as Kripke Structures -- 3.3 The Proposed Logic: A Two-Level Temporal Logic for Specifications Checking -- 3.4 Examples -- 4 Conclusion and Future Works -- References -- Statistical Model Checking for Traffic Models -- 1 Introduction -- 2 Background -- 2.1 SMC and MultiVeStA -- 2.2 SUMO - Simulation of Urban MObility -- 2.3 Car-Following and Lane Changing Models -- 3 Integration of MultiVeStA and SUMO Simulator -- 3.1 Initial Step -- 3.2 Integration -- 4 Simulation Experiments and Results -- 4.1 Simple Queries -- 4.2 Query 1: Behaviour on Emergency Vehicles -- 4.3 Query 2: Traffic Load Comparison -- 4.4 Query 3: Load Conditions for Traffic Jams -- 4.5 Query 4: Impending Drop in Traffic -- 4.6 Running Times -- 5 Conclusion and Future Work -- References -- Visual Specification of Properties for Robotic Designs -- 1 Introduction -- 2 Background -- 2.1 RoboChart -- 2.2 UML Activity Diagram -- 2.3 CSP Notation, Templates and Tools Used in the Work -- 3 Diagrammatic Language for Properties -- 3.1 Language Syntax -- 3.2 Language Semantics -- 4 Tool Support -- 5 Related Work -- 6 Conclusion -- References -- Model Checking and Strategy Synthesis for Multi-agent Systems for Resource Allocation -- 1 Introduction -- 2 Multi-agent Systems for Resource Allocation -- 3 Propositional Logic Encoding -- 3.1 Overall Encoding -- 3.2 Basic Encodings -- 3.3 Properties of the Encoding -- 4 Algorithm -- 5 Implementation and Experiments -- 6 Related Work -- 7 Conclusion and Outlook -- References.
Temporal Reasoning Through Automatic Translation of tock-CSP into Timed Automata -- 1 Introduction -- 2 Background -- 3 An Overview of the Translation Technique -- 4 Evaluation -- 4.1 Experimental Evaluation -- 4.2 Mathematical Proof -- 5 Related Work and Conclusions -- References -- Module Integration Using Graph Grammars (MIGRATE) -- 1 Introduction -- 2 Graph Grammars -- 3 Illustration of the Proposed Approach -- 4 Module Nets -- 5 MIGRATE Approach -- 5.1 Translation -- 5.2 Verification -- 6 Related Work -- 7 Conclusion -- References -- Cost Analysis for an Actor-Based Workflow Modelling Language -- 1 Introduction -- 2 Formal Workflow Modelling Language Rpl -- 2.1 The Syntax of Rpl -- 2.2 The Semantics of Rpl -- 3 Analysis of Rpl Program -- 3.1 Synchronisation Schema -- 3.2 Accumulated Costs -- 3.3 Translation Function -- 4 Properties -- 5 Related Work -- 6 Conclusion -- References -- Minimization of the Number of Clocks for Timed Scenarios -- 1 Introduction -- 2 Preliminaries -- 2.1 Timed Automata -- 2.2 Timed Scenarios -- 3 A New Optimization Algorithm -- 3.1 Cyclic Dependencies -- 3.2 Cyclic Dependencies and Equality Constraints -- 3.3 C(Ds) with Cyclic Dependencies -- 3.4 Resolving Cyclic Dependencies -- 3.5 The Optimization Algorithm -- 4 Conclusions -- References -- Author Index. |
| Record Nr. | UNINA-9910510573403321 |
| Cham, Switzerland : , : Springer, , [2021] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Formal methods : foundations and applications : 23rd Brazilian symposium, SBMF 2020, Ouro Preto, Brazil, November 25-27, 2020, proceedings. / / Gustavo Carvalho, Volker Stolz (editors)
| Formal methods : foundations and applications : 23rd Brazilian symposium, SBMF 2020, Ouro Preto, Brazil, November 25-27, 2020, proceedings. / / Gustavo Carvalho, Volker Stolz (editors) |
| Edizione | [1st ed. 2020.] |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2020] |
| Descrizione fisica | 1 online resource (X, 229 p. 432 illus.) |
| Disciplina | 004.0151 |
| Collana | Lecture notes in computer science |
| Soggetto topico | Formal methods (Computer science) |
| ISBN | 3-030-63882-0 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- Formal Verification of Neural Networks? -- Navigating the Universe of Z3 Theory Solvers -- Revisiting Refactoring Mechanics from Tool Developers' Perspective -- Experience Reports -- Safety Assurance of a High Voltage Controller for an Industrial Robotic System -- Statistical Model Checking in Drug Repurposing for Alzheimer's Disease -- Models, Languages and Semantics -- Calculational Proofs in Relational Graphical Linear Algebra -- Modeling Big Data Processing Programs -- Optimization of Timed Scenarios -- Reversal Fuzzy Switch Graphs -- Separation Logic-Based Verification atop a Binary-Compatible Filesystem Model -- Software Product Lines -- Merging Cloned Alloy Models with Colorful Refactorings -- Porting the Software Product Line Refinement Theory to the Coq Proof Assistant -- Safe Evolution of Product Lines using Configuration Knowledge Laws. |
| Record Nr. | UNISA-996418210003316 |
| Cham, Switzerland : , : Springer, , [2020] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Formal methods : foundations and applications : 23rd Brazilian symposium, SBMF 2020, Ouro Preto, Brazil, November 25-27, 2020, proceedings. / / Gustavo Carvalho, Volker Stolz (editors)
| Formal methods : foundations and applications : 23rd Brazilian symposium, SBMF 2020, Ouro Preto, Brazil, November 25-27, 2020, proceedings. / / Gustavo Carvalho, Volker Stolz (editors) |
| Edizione | [1st ed. 2020.] |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2020] |
| Descrizione fisica | 1 online resource (X, 229 p. 432 illus.) |
| Disciplina | 004.0151 |
| Collana | Lecture notes in computer science |
| Soggetto topico | Formal methods (Computer science) |
| ISBN | 3-030-63882-0 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- Formal Verification of Neural Networks? -- Navigating the Universe of Z3 Theory Solvers -- Revisiting Refactoring Mechanics from Tool Developers' Perspective -- Experience Reports -- Safety Assurance of a High Voltage Controller for an Industrial Robotic System -- Statistical Model Checking in Drug Repurposing for Alzheimer's Disease -- Models, Languages and Semantics -- Calculational Proofs in Relational Graphical Linear Algebra -- Modeling Big Data Processing Programs -- Optimization of Timed Scenarios -- Reversal Fuzzy Switch Graphs -- Separation Logic-Based Verification atop a Binary-Compatible Filesystem Model -- Software Product Lines -- Merging Cloned Alloy Models with Colorful Refactorings -- Porting the Software Product Line Refinement Theory to the Coq Proof Assistant -- Safe Evolution of Product Lines using Configuration Knowledge Laws. |
| Record Nr. | UNINA-9910427671103321 |
| Cham, Switzerland : , : Springer, , [2020] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Formal Methods and Software Engineering : 24th International Conference on Formal Engineering Methods, ICFEM 2023, Brisbane, QLD, Australia, November 21-24, 2023, Proceedings / / Yi Li and Sofiène Tahar, editors
| Formal Methods and Software Engineering : 24th International Conference on Formal Engineering Methods, ICFEM 2023, Brisbane, QLD, Australia, November 21-24, 2023, Proceedings / / Yi Li and Sofiène Tahar, editors |
| Edizione | [First edition.] |
| Pubbl/distr/stampa | Singapore : , : Springer, , [2024] |
| Descrizione fisica | 1 online resource (319 pages) |
| Disciplina | 004.0151 |
| Collana | Lecture Notes in Computer Science Series |
| Soggetto topico |
Formal methods (Computer science)
Software engineering |
| ISBN | 981-9975-84-0 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talk: Verifying Compiler Optimisations -- Regular Papers: An Idealist’s Approach for Smart Contract Correctness -- Active Inference of EFSMs Without Reset -- Learning Mealy Machines with Local Timers -- Compositional Vulnerability Detection with Insecurity Separation Logic -- Dynamic Extrapolation in Extended Timed Automata -- Formalizing Robustness against Character-level Perturbations for Neural Network Language Models -- Trace models of concurrent valuation algebras -- Branch and Bound for Sigmoid-like Neural Network Verification -- Certifying Sequential Consistency of Machine Learning Accelerators -- Guided Integration of Formal Verification in Assurance Cases -- Validation-Driven Development -- Incremental Property Directed Reachability -- Proving Local Invariants in ASTDs -- Doctoral Symposium Papers: Formal Verification of the Burn-to-Claim Blockchain Interoperable Protocol -- Early and systematic validation of formal models -- Verifying Neural Networks by Approximating Convex Hulls -- Eager to Stop: Efficient Falsification of Deep Neural Networks -- A Runtime Verification Framework For Cyber-physical Systems Based On Data Analytics And LTL Formula Learning -- Unified Verification of Neural Networks’ Robustness and Privacy in Computer Vision -- IoT Software Vulnerability Detection Techniques through Large Language Model -- Vulnerability Detection via Typestate-Guided Code Representation Learning. |
| Record Nr. | UNISA-996565870603316 |
| Singapore : , : Springer, , [2024] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
