


default search action
FM 2023: Lübeck, Germany
- Marsha Chechik

, Joost-Pieter Katoen
, Martin Leucker
:
Formal Methods - 25th International Symposium, FM 2023, Lübeck, Germany, March 6-10, 2023, Proceedings. Lecture Notes in Computer Science 14000, Springer 2023, ISBN 978-3-031-27480-0
Keynotes
- Laura Kovács:

Symbolic Computation in Automated Program Reasoning. 3-9 - Harald Ruess:

The Next Big Thing: From Embedded Systems to Embodied Actors. 10-25 - Nils Jansen

:
Intelligent and Dependable Decision-Making Under Uncertainty. 26-36
SAT/SMT
- Sylvie Boldo

, François Clément, Vincent Martin, Micaela Mayero, Houda Mouhcine:
A Coq Formalization of Lebesgue Induction Principle and Tonelli's Theorem. 39-55 - Tomás Kolárik

, Stefan Ratschan
:
Railway Scheduling Using Boolean Satisfiability Modulo Simulations. 56-73 - Matan Peled

, Bat-Chen Rothenberg
, Shachar Itzhaky
:
SMT Sampling via Model-Guided Approximation. 74-91 - Yu Liu, Pavle Subotic

, Emmanuel Letier
, Sergey Mechtaev
, Abhik Roychoudhury
:
Efficient SMT-Based Network Fault Tolerance Verification. 92-100
Verification I
- Robert Sison

, Scott Buckley
, Toby Murray
, Gerwin Klein
, Gernot Heiser
:
Formalising the Prevention of Microarchitectural Timing Channels by Operating Systems. 103-121 - Maurice H. ter Beek

, Guillermina Cledou
, Rolf Hennicker, José Proença
:
Can We Communicate? Using Dynamic Logic to Verify Team Automata. 122-141 - Gianluca Amato

, Francesca Scozzari
:
The ScalaFix Equation Solver. 142-159 - Huanhuan Sheng, Alexander Bentkamp, Bohua Zhan:

HHLPy: Practical Verification of Hybrid Systems Using Hoare Logic. 160-178
Quantitative Verification
- Fabian Bauer-Marquart

, Stefan Leue
, Christian Schilling
:
symQV: Automated Symbolic Verification of Quantum Programs. 181-198 - Stefano M. Nicoletti

, Milan Lopuhaä-Zwakenberg
, Ernst Moritz Hahn
, Mariëlle Stoelinga
:
sfPFL: A Probabilistic Logic for Fault Trees. 199-221 - Sven Dziadek

, Uli Fahrenberg
, Philipp Schlehuber-Caissier
:
Energy Büchi Problems. 222-239 - Rubén Rubio

, Narciso Martí-Oliet
, Isabel Pita
, Alberto Verdejo
:
QMaude: Quantitative Specification and Verification in Rewriting Logic. 240-259
Concurrency and Memory Models
- Vincenzo Ciancia

, Jan Friso Groote
, Diego Latella
, Mieke Massink
, Erik P. de Vink
:
Minimisation of Spatial Models Using Branching Bisimilarity. 263-281 - Heike Wehrheim

, Lara Bargmann, Brijesh Dongol
:
Reasoning About Promises in Weak Memory Models with Event Structures. 282-300 - Robert J. Colvin:

A Fine-Grained Semantics for Arrays and Pointers Under Weak Memory Models. 301-320 - Petra van den Bos, Sung-Shik Jongmans:

VeyMont: Parallelising Verified Programs Instead of Verifying Parallel Programs. 321-339
Verification 2
- Marco Paganoni, Carlo A. Furia

:
Verifying Functional Correctness Properties at the Level of Java Bytecode. 343-363 - Jan Oliver Ringert

, Allison Sullivan
:
Abstract Alloy Instances. 364-382 - David A. Basin

, Daniel Stefan Dietiker
, Srdan Krstic
, Yvonne-Anne Pignolet
, Martin Raszyk
, Joshua Schneider
, Arshavir Ter-Gabrielyan
:
Monitoring the Internet Computer. 383-402 - Frantisek Blahoudek, Yu-Fang Chen, David Chocholatý

, Vojtech Havlena, Lukás Holík, Ondrej Lengál, Juraj Síc
:
Word Equations in Synergy with Regular Constraints. 403-423
Formal Methods in AI
- Achim D. Brucker

, Amy Stell
:
Verifying Feedforward Neural Networks for Classification in Isabelle/HOL. 427-444 - Nicolas Amat

, Silvano Dal-Zilio
:
SMPT: A Testbed for Reachability Methods in Generalized Petri Nets. 445-453 - Stanley Bak

, Taylor Dohmen
, K. Subramani, Ashutosh Trivedi
, Alvaro Velasquez, Piotr Wojciechowski:
The Octatope Abstract Domain for Verification of Neural Networks. 454-472 - Solofomampionona Fortunat Rajaona

, Ioana Boureanu
, Vadim Malvone, Francesco Belardinelli:
Program Semantics and Verification Technique for AI-Centred Programs. 473-491
Safety and Reliability
- Montserrat Hermo

, Paqui Lucio
, César Sánchez
:
Tableaux for Realizability of Safety Specifications. 495-513 - Sebastiaan Brand

, Thomas Bäck
, Alfons Laarman
:
A Decision Diagram Operation for Reachability. 514-532 - Tsutomu Kobayashi

, Martin Bondu, Fuyuki Ishikawa
:
Formal Modelling of Safety Architecture for Responsibility-Aware Autonomous Vehicle via Event-B Refinement. 533-549 - Davide Basile

, Maurice H. ter Beek
:
A Runtime Environment for Contract Automata. 550-567
Industry Day
- Franck Cassez

, Joanne Fuller, Milad K. Ghale, David J. Pearce
, Horacio Mijail Anton Quiles:
Formal and Executable Semantics of the Ethereum Virtual Machine in Dafny. 571-583 - Ben Liblit, Linghui Luo

, Alejandro Molina, Rajdeep Mukherjee, Zachary Patterson, Goran Piskachev, Martin Schäf, Omer Tripp, Willem Visser:
Shifting Left for Early Detection of Machine-Learning Bugs. 584-597 - Masoud Ebrahimi, Stefan Marksteiner

, Dejan Nickovic
, Roderick Bloem, David Schögler, Philipp Eisner, Samuel Sprung, Thomas Schober, Sebastian Chlup, Christoph Schmittner, Sandra König
:
A Systematic Approach to Automotive Security. 598-609 - Adam Molin, Edgar A. Aguilar, Dejan Nickovic

, Mengjia Zhu
, Alberto Bemporad, Hasan Esen:
Specification-Guided Critical Scenario Identification for Automated Driving. 610-621 - Vahid Hashemi, Jan Kretínský, Sabine Rieder

, Jessica Schmidt:
Runtime Monitoring for Out-of-Distribution Detection in Object Detection Neural Networks. 622-634 - Akshay Dhonthi, Ernst Moritz Hahn, Vahid Hashemi:

Backdoor Mitigation in Deep Neural Networks via Strategic Retraining. 635-647 - Guy Amir, Ziv Freund, Guy Katz, Elad Mandelbaum, Idan Refaeli:

veriFIRE: Verifying an Industrial, Learning-Based Wildfire Detection System. 648-656

manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.


Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID














