Cover Image

Formal Methods : 25th International Symposium, FM 2023, Lübeck, Germany, March 6-10, 2023, Proceedings /

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...

Full description

Bibliographic Details
Corporate Author: SpringerLink (Online service)
Other Authors: Chechik, Marsha (Editor), Katoen, Joost-Pieter (Editor), Leucker, Martin (Editor)
Format: eBook
Language:English
Published: Cham : Springer International Publishing : Imprint: Springer, 2023.
Edition:1st ed. 2023.
Series:Lecture Notes in Computer Science, 14000
Subjects:
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).
Electronic books.
Online Access:Connect to the full text of this electronic book
Table of Contents:
  • 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.