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.