Vai al contenuto principale della pagina
| Titolo: |
Formal Methods : 25th International Symposium, FM 2023, Lübeck, Germany, March 6–10, 2023, Proceedings / / edited by Marsha Chechik, Joost-Pieter Katoen, Martin Leucker
|
| Pubblicazione: | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2023 |
| Edizione: | 1st ed. 2023. |
| Descrizione fisica: | 1 online resource (661 pages) |
| Disciplina: | 004.0151 |
| Soggetto topico: | Software engineering |
| Computer science | |
| Computers, Special purpose | |
| Programming languages (Electronic computers) | |
| Microprogramming | |
| Natural language processing (Computer science) | |
| Software Engineering | |
| Computer Science Logic and Foundations of Programming | |
| Special Purpose and Application-Based Systems | |
| Programming Language | |
| Control Structures and Microprogramming | |
| Natural Language Processing (NLP) | |
| Persona (resp. second.): | KatoenJoost-Pieter |
| LeuckerMartin | |
| ChechikMarsha | |
| Nota di bibliografia: | Includes bibliographical references and index. |
| 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 BuechiProblems -- 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. |
| Sommario/riassunto: | This book constitutes the refereed proceedings of the 25th International Symposium on Formal Methods, FM 2023, which took place in Lübeck, Germany, in March 2023. The 26 full paper, 2 short papers included in this book were carefully reviewed and selected rom 95 submissions. They have been organized in topical sections as follows: SAT/SMT; Verification; Quantitative Verification; Concurrency and Memory Models; Formal Methods in AI; Safety and Reliability. The proceedings also contain 3 keynote talks and 7 papers from the industry day. . |
| Titolo autorizzato: | Formal methods ![]() |
| ISBN: | 9783031274817 |
| 3031274814 | |
| Formato: | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione: | Inglese |
| Record Nr.: | 9910678257703321 |
| Lo trovi qui: | Univ. Federico II |
| Opac: | Controlla la disponibilità qui |