


default search action
15th NFM 2023: Houston, TX, USA
- Kristin Yvonne Rozier
, Swarat Chaudhuri
:
NASA Formal Methods - 15th International Symposium, NFM 2023, Houston, TX, USA, May 16-18, 2023, Proceedings. Lecture Notes in Computer Science 13903, Springer 2023, ISBN 978-3-031-33169-5 - Farzaneh Moradkhani
, Connor Fibich
, Martin Fränzle
:
Verification of LSTM Neural Networks with Non-linear Activation Functions. 1-15 - Niklas Kochdumper, Christian Schilling
, Matthias Althoff, Stanley Bak:
Open- and Closed-Loop Neural Network Verification Using Polynomial Zonotopes. 16-36 - Satoshi Munakata, Caterina Urban, Haruki Yokoyama, Koji Yamamoto, Kazuki Munakata:
Verifying Attention Robustness of Deep Neural Networks Against Semantic Perturbations. 37-61 - Andrei Aleksandrov
, Kim Völlinger
:
Formalizing Piecewise Affine Activation Functions of Neural Networks in Coq. 62-78 - Cong Liu, Darren D. Cofer, Denis Osipychev:
Verifying an Aircraft Collision Avoidance Neural Network with Marabou. 79-85 - Christel Baier
, Clemens Dubslaff, Patrick Wienhöft
, Stefan J. Kiebel:
Strategy Synthesis in Markov Decision Processes Under Limited Sampling Access. 86-103 - Simon Dierl
, Falk Maria Howar
, Sean Kauffman
, Martin Kristjansen
, Kim Guldstrand Larsen
, Florian Lorber
, Malte Mauritz
:
Learning Symbolic Timed Models from Concrete Timed Data. 104-121 - Marian Qian
, Stefan Mitsch
:
Reward Shaping from Hybrid Systems Models in Reinforcement Learning. 122-139 - Matthew Cleaveland, Oleg Sokolsky, Insup Lee, Ivan Ruchkin
:
Conservative Safety Monitors of Stochastic Dynamical Systems. 140-156 - Elias Khalife, Pierre-Loïc Garoche, Mazen Farhood:
Code-Level Formal Verification of Ellipsoidal Invariant Sets for Linear Parameter-Varying Systems. 157-173 - Alberto Bombardelli
, Stefano Tonetta
:
Reasoning with Metric Temporal Logic and Resettable Skewed Clocks. 174-190 - Alexandra Forsey-Smerek
, Ho Chit Siu
, Kevin Leahy
:
Centralized Multi-agent Synthesis with Spatial Constraints via Mixed-Integer Quadratic Programming. 191-206 - Anna Fritz, Perry Alexander
:
A Framework for Policy Based Negotiation. 207-223 - Kevin Leahy
, Makai Mann
, Cristian-Ioan Vasile
:
Rewrite-Based Decomposition of Signal Temporal Logic Specifications. 224-240 - Blair Archibald, Muffy Calder, Michele Sevegnani, Mengwei Xu
:
Quantitative Verification and Strategy Synthesis for BDI Agents. 241-259 - Thomas Robinson
, Guoxin Su
:
Multi-objective Task Assignment and Multiagent Planning with Hybrid GPU-CPU Acceleration. 260-277 - Apurva Badithela, Josefine B. Graebener, Inigo Incer
, Richard M. Murray:
Reasoning over Test Specifications Using Assume-Guarantee Contracts. 278-294 - Felipe Lisboa Malaquias
, Mihail Asavoae
, Florian Brandner
:
From the Standards to Silicon: Formally Proved Memory Controllers. 295-311 - Peter Riviere, Neeraj Kumar Singh, Yamine Aït Ameur, Guillaume Dupont:
Formalising Liveness Properties in Event-B with the Reflexive EB4EB Framework. 312-331 - William L. Harrison
, Ian Blumenfeld
, Eric Bond
, Chris Hathhorn
, Paul Li
, May Torrence, Jared Ziegler:
Formalized High Level Synthesis with Applications to Cryptographic Hardware. 332-352 - Zsófia Ádám
, Ignacio D. Lopez-Miguel
, Anastasia Mavridou, Thomas Pressburger, Marcin Bes, Enrique Blanco Viñuela, Andreas Katis
, Jean-Charles Tournier, Khanh V. Trinh, Borja Fernández Adiego:
From Natural Language Requirements to the Verification of Programmable Logic Controllers: Integrating FRET into PLCverif. 353-360 - Bernd Finkbeiner
, Hadar Frenkel
, Jana Hofmann
, Janine Lohse
:
Automata-Based Software Model Checking of Hyperproperties. 361-379 - Bat-Chen Rothenberg, Orna Grumberg, Yakir Vizel, Eytan Singher
:
Condition Synthesis Realizability via Constrained Horn Clauses. 380-396 - Aleksandr Fedchin, Tyler Dean, Jeffrey S. Foster, Eric Mercer, Zvonimir Rakamaric, Giles Reger, Neha Rungta, Robin Salkeld, Lucas Wagner, Cassidy Waldrip:
A Toolkit for Automated Testing of Dafny. 397-413 - Sam Lasser, Chris Casinghino, Derek Egolf, Kathleen Fisher, Cody Roux:
Verified ALL(*) Parsing with Semantic Actions and Dynamic Input Validation. 414-429 - Jasper Nalbach
, Erika Ábrahám
:
Subtropical Satisfiability for SMT Solving. 430-446 - Md. Solimul Chowdhury
, Cayden R. Codel
, Marijn J. H. Heule
:
A Linear Weight Transfer Rule for Local Search. 447-463 - Steffan Christ Sølvsten
, Jaco van de Pol
:
Adiar 1.1 - Zero-Suppressed Decision Diagrams in External Memory. 464-471 - Enrico Lipparini
, Stefan Ratschan
:
Satisfiability of Non-linear Transcendental Arithmetic as a Certificate Search Problem. 472-488

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.